Let m be given.
Let q be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Let r be given.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim LqN:
nat_p q.
An
exact proof term for the current goal is
omega_nat_p q Hq.
We prove the intermediate
claim LrN:
nat_p r.
An
exact proof term for the current goal is
nat_p_trans n LnN r Hr.
We prove the intermediate
claim L1:
m = q * n + r.
Use transitivity with and
mul_nat q n + r.
rewrite the current goal using H1 (from left to right).
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hr.
We will
prove m = q * n + r.
An exact proof term for the current goal is L1.
Let m be given.
Let q be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Let r be given.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim LqN:
nat_p q.
An
exact proof term for the current goal is
omega_nat_p q Hq.
We prove the intermediate
claim LqS:
SNo q.
An exact proof term for the current goal is LqN.
We prove the intermediate
claim LrN:
nat_p r.
An
exact proof term for the current goal is
nat_p_trans n LnN r Hr.
We prove the intermediate
claim LrS:
SNo r.
An exact proof term for the current goal is LrN.
We prove the intermediate
claim LnS:
SNo n.
An exact proof term for the current goal is LnN.
We prove the intermediate
claim LqnS:
SNo (q * n).
An
exact proof term for the current goal is
SNo_mul_SNo q n LqS LnS.
We prove the intermediate
claim L2:
m = q * n + r.
Use transitivity with and
mul_nat q n + r.
rewrite the current goal using H1 (from left to right).
We prove the intermediate
claim L3:
0 ≤ r.
An exact proof term for the current goal is LrN.
We prove the intermediate
claim L4:
n + - r ∈ n.
An exact proof term for the current goal is Hn1.
An exact proof term for the current goal is LrN.
We will
prove 0 ≤ n + - r.
rewrite the current goal using
add_SNo_0L r LrS (from left to right).
An exact proof term for the current goal is Lno.
We will
prove n + - r < n.
rewrite the current goal using
add_SNo_0R n LnS (from right to left) at position 1.
We will
prove n + 0 < n + r.
We use
(- q + - 1) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
An
exact proof term for the current goal is
nat_1.
We use
(n + - r) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is L4.
We will
prove - m = ((- q) * n + (- 1) * n) + (n + - r).
rewrite the current goal using
mul_SNo_oneL n LnS (from left to right).
We will
prove - m = (- q * n + - n) + (n + - r).
We will
prove - m = - q * n + - r.
Use f_equal.
An exact proof term for the current goal is L2.
We use
(- q) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
We use
0 to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is L0n.
We will
prove - m = (- q) * n + 0.
We will
prove - m = - (q * n) + 0.
rewrite the current goal using L2 (from left to right).
We will
prove - (q * n + r) = - (q * n) + 0.
rewrite the current goal using H2 (from right to left).
rewrite the current goal using
add_SNo_0R (q * n) LqnS (from left to right).
Use symmetry.
∎