We prove the intermediate
claim LnZ:
n ∈ int.
We prove the intermediate
claim LnnS:
SNo (n * n).
An
exact proof term for the current goal is
SNo_mul_SNo n n LnS LnS.
We prove the intermediate
claim Lm:
m ∈ ω.
An
exact proof term for the current goal is
nat_p_omega m Hm.
We prove the intermediate
claim LmZ:
m ∈ int.
We prove the intermediate
claim LmS:
SNo m.
An
exact proof term for the current goal is
nat_p_SNo m Hm.
We prove the intermediate
claim Lmpos:
0 < m.
An exact proof term for the current goal is H3.
We will
prove m * m < m * m.
rewrite the current goal using H1 (from left to right) at position 2.
We will
prove m * m < 2 * n * n.
rewrite the current goal using H3 (from right to left) at position 2.
We will
prove m * 0 < 2 * n * n.
rewrite the current goal using
mul_SNo_zeroR m LmS (from left to right).
We will
prove 0 < 2 * n * n.
An
exact proof term for the current goal is
mul_SNo_pos_pos n n LnS LnS H2 H2.
We prove the intermediate
claim Lm2pos:
0 < m :/: 2.
We prove the intermediate
claim Ln2pos:
0 < n :/: 2.
rewrite the current goal using H1 (from left to right).
We will
prove n * n ∈ int.
An exact proof term for the current goal is Ln.
An exact proof term for the current goal is Ln.
An
exact proof term for the current goal is
nat_2.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is H3.
We prove the intermediate
claim Lm2Z:
m :/: 2 ∈ int.
We prove the intermediate
claim Lm2N:
nat_p (m :/: 2).
An exact proof term for the current goal is Lm2pos.
We prove the intermediate
claim Lm2S:
SNo (m :/: 2).
An
exact proof term for the current goal is
nat_p_SNo (m :/: 2) Lm2N.
We prove the intermediate
claim Lm2m:
m :/: 2 ∈ m.
We will
prove m :/: 2 < m.
We will
prove m + - m < m * 2 + - m.
We will
prove 0 < m * 2 + - m.
rewrite the current goal using
mul_SNo_oneR m LmS (from right to left) at position 2.
rewrite the current goal using
add_SNo_1_1_2 (from right to left).
rewrite the current goal using
mul_SNo_oneR m LmS (from left to right).
An exact proof term for the current goal is Lmpos.
Apply and3I to the current goal.
An
exact proof term for the current goal is
nat_2.
We will
prove n * n ∈ int.
An exact proof term for the current goal is LnZ.
An exact proof term for the current goal is LnZ.
We use
(m :/: 2) * (m :/: 2) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lm2Z.
An exact proof term for the current goal is Lm2Z.
We will
prove m * (m :/: 2) = n * n.
We will
prove (m * m) :/: 2 = n * n.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is H3.
An exact proof term for the current goal is H3.
We prove the intermediate
claim Ln2Z:
n :/: 2 ∈ int.
We prove the intermediate
claim Ln2N:
nat_p (n :/: 2).
An exact proof term for the current goal is Ln2pos.
rewrite the current goal using H1 (from left to right).
Use symmetry.
We prove the intermediate
claim Ln20:
n :/: 2 = 0.
An
exact proof term for the current goal is
IHm (m :/: 2) Lm2m (n :/: 2) Ln2N L1.
rewrite the current goal using Ln20 (from right to left) at position 2.