Documentation
Acmoi
.
Exercise1_3
Search
Google site search
return to top
source
Imports
Init
Mathlib.Tactic.Linarith
Mathlib.Tactic.Ring
Mathlib.Data.Int.ModEq
Imported by
lemma_1_52
source
theorem
lemma_1_52
(r :
ℤ
)
(x :
ℤ
)
(y :
ℤ
)
(hr :
0
<
r
)
(hy :
0
≤
y
)
(hx :
0
≤
x
)
:
2
*
r
^
2
=
(
x
+
y
)
*
r
+
(
y
+
1
)
↔
(
x
,
y
)
=
(
r
,
r
-
1
)