Documentation
Acmoi
.
Exercise3_1_2
Search
return to top
source
Imports
Init
Mathlib.Data.Finset.Card
Mathlib.Data.Fintype.Basic
Mathlib.Data.Fintype.Prod
Imported by
sat_eq
unique_sol
paireq
proj1eq
proj2eq
reduce
amplify
source
def
sat_eq
(
a
:
ℕ
×
ℕ
)
(
n
:
ℕ
)
(
x
:
ℕ
×
ℕ
)
:
Prop
Equations
sat_eq
a
n
x
=
(
a
.1
*
x
.1
+
a
.2
*
x
.2
=
n
)
Instances For
source
def
unique_sol
(
a
:
ℕ
×
ℕ
)
(
n
:
ℕ
)
:
Prop
Equations
unique_sol
a
n
=
∃!
x
:
ℕ
×
ℕ
,
sat_eq
a
n
x
Instances For
source
theorem
paireq
(
a
b
c
d
:
ℕ
)
(
ha
:
a
=
c
)
(
hb
:
b
=
d
)
:
(
a
,
b
)
=
(
c
,
d
)
source
theorem
proj1eq
{
a
b
c
d
:
ℕ
}
(
h
:
(
a
,
b
)
=
(
c
,
d
)
)
:
a
=
c
source
theorem
proj2eq
{
a
b
c
d
:
ℕ
}
(
h
:
(
a
,
b
)
=
(
c
,
d
)
)
:
b
=
d
source
theorem
reduce
(
a
:
ℕ
×
ℕ
)
(
n
x₀
u
v
:
ℕ
)
(
original
:
unique_sol
a
(
n
+
a
.2
*
v
)
∧
sat_eq
a
(
n
+
a
.2
*
v
)
(
x₀
,
u
+
v
)
)
:
unique_sol
a
n
source
theorem
amplify
(
a
:
ℕ
×
ℕ
)
(
n
x₀
u
v
:
ℕ
)
(
u_pos
:
0
<
u
)
(
original
:
unique_sol
a
n
∧
sat_eq
a
n
(
x₀
,
u
*
v
)
)
:
unique_sol
(
a
.1
,
a
.2
*
u
)
n