Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/Array.mapIdx
/
.
/
tests
/
lean
/
hpow.lean.expected.out
blob: 582c8982567aa9b57e38d97a40908b18de08f2f0 [
file
] [
edit
]
↑
n
^
2
+
m
^
2
:
Int
n
^
2
+
1
:
Nat
↑
n
^
2
+
1
:
Int
↑
n
^
2
+
↑
1
:
Int
q
^
n
+
1
:
Rat
q
^
m
+
1
:
Rat
q
^
↑
n
+
1
:
Rat
12
*
q
+
1
≤
13
*
q
^
2
:
Prop
12
*
q
+
1
≤
13
*
q
^
2
:
Prop