Assume H2: 0 < n.

We will prove False.

We prove the intermediate claim LnZ: n ∈ int.

An exact proof term for the current goal is Subq_omega_int n Ln.

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.

An exact proof term for the current goal is Subq_omega_int m Lm.

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.

Apply SNoLeE 0 m SNo_0 LmS (omega_nonneg m Lm) to the current goal.

Assume H3: 0 < m.

An exact proof term for the current goal is H3.

Assume H3: 0 = m.

We will prove False.

Apply SNoLt_irref (m * m) to the current goal.

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.

Apply mul_SNo_pos_pos 2 (n * n) SNo_2 LnnS SNoLt_0_2 to the current goal.

We will prove 0 < 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.

An exact proof term for the current goal is div_SNo_pos_pos m 2 LmS SNo_2 Lmpos SNoLt_0_2.

We prove the intermediate claim Ln2pos: 0 < n :/: 2.

An exact proof term for the current goal is div_SNo_pos_pos n 2 LnS SNo_2 H2 SNoLt_0_2.

We prove the intermediate claim L2mm: divides_int 2 (m * m).

We will prove divides_int 2 (m * m).

rewrite the current goal using H1 (from left to right).

We will prove divides_int 2 (2 * n * n).

Apply divides_int_mul_SNo_L to the current goal.

We will prove n * n ∈ int.

Apply Subq_omega_int to the current goal.

Apply mul_SNo_In_omega to the current goal.

An exact proof term for the current goal is Ln.

We will prove divides_int 2 2.

Apply divides_int_ref to the current goal.

We will prove 2 ∈ int.

Apply Subq_omega_int to the current goal.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_2.

We prove the intermediate claim L2m: divides_int 2 m.

Apply Euclid_lemma 2 prime_nat_2 m LmZ m LmZ L2mm to the current goal.

Assume H3: divides_int 2 m.

An exact proof term for the current goal is H3.

Assume H3: divides_int 2 m.

An exact proof term for the current goal is H3.

We prove the intermediate claim Lm2Z: m :/: 2 ∈ int.

An exact proof term for the current goal is divides_int_div_SNo_int 2 m L2m.

We prove the intermediate claim Lm2N: nat_p (m :/: 2).

Apply nonneg_int_nat_p (m :/: 2) Lm2Z to the current goal.

We will prove 0 ≤ m :/: 2.

Apply SNoLtLe to the current goal.

We will prove 0 < 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.

Apply ordinal_SNoLt_In (m :/: 2) m (nat_p_ordinal (m :/: 2) Lm2N) (nat_p_ordinal m Hm) to the current goal.

We will prove m :/: 2 < m.

Apply div_SNo_pos_LtL m 2 m LmS SNo_2 LmS SNoLt_0_2 to the current goal.

We will prove m < m * 2.

Apply add_SNo_Lt1_cancel m (- m) (m * 2) LmS (SNo_minus_SNo m LmS) (SNo_mul_SNo m 2 LmS SNo_2) to the current goal.

We will prove m + - m < m * 2 + - m.

rewrite the current goal using add_SNo_minus_SNo_rinv m LmS (from left to right).

We will prove 0 < m * 2 + - m.

rewrite the current goal using mul_SNo_oneR m LmS (from right to left) at position 2.

We will prove 0 < m * 2 + - m * 1.

rewrite the current goal using mul_SNo_minus_distrR m 1 LmS SNo_1 (from right to left).

We will prove 0 < m * 2 + m * (- 1).

rewrite the current goal using mul_SNo_distrL m 2 (- 1) LmS SNo_2 (SNo_minus_SNo 1 SNo_1) (from right to left).

We will prove 0 < m * (2 + - 1).

rewrite the current goal using add_SNo_1_1_2 (from right to left).

We will prove 0 < m * ((1 + 1) + - 1).

rewrite the current goal using add_SNo_minus_R2 1 1 SNo_1 SNo_1 (from left to right).

We will prove 0 < m * 1.

rewrite the current goal using mul_SNo_oneR m LmS (from left to right).

We will prove 0 < m.

An exact proof term for the current goal is Lmpos.

We prove the intermediate claim L2nn: divides_int 2 (n * n).

We will prove divides_int 2 (n * n).

We will prove 2 ∈ int ∧ n * n ∈ int ∧ ∃k ∈ int, 2 * k = n * n.

Apply and3I to the current goal.

We will prove 2 ∈ int.

Apply Subq_omega_int to the current goal.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_2.

We will prove n * n ∈ int.

Apply int_mul_SNo to the current goal.

An exact proof term for the current goal is LnZ.

We will prove ∃k ∈ int, 2 * k = n * n.

We use (m :/: 2) * (m :/: 2) to witness the existential quantifier.

Apply andI to the current goal.

We will prove (m :/: 2) * (m :/: 2) ∈ int.

Apply int_mul_SNo to the current goal.

An exact proof term for the current goal is Lm2Z.

We will prove 2 * ((m :/: 2) * (m :/: 2)) = n * n.

rewrite the current goal using mul_SNo_assoc 2 (m :/: 2) (m :/: 2) SNo_2 Lm2S Lm2S (from left to right).

We will prove (2 * (m :/: 2)) * (m :/: 2) = n * n.

rewrite the current goal using mul_div_SNo_invR m 2 LmS SNo_2 neq_2_0 (from left to right).

We will prove m * (m :/: 2) = n * n.

rewrite the current goal using mul_div_SNo_L m 2 m LmS SNo_2 LmS (from left to right).

We will prove (m * m) :/: 2 = n * n.

rewrite the current goal using H1 (from left to right).

We will prove (2 * n * n) :/: 2 = n * n.

rewrite the current goal using mul_SNo_com 2 (n * n) SNo_2 LnnS (from left to right).

We will prove ((n * n) * 2) :/: 2 = n * n.

An exact proof term for the current goal is div_mul_SNo_invL (n * n) 2 LnnS SNo_2 neq_2_0.

We prove the intermediate claim L2n: divides_int 2 n.

Apply Euclid_lemma 2 prime_nat_2 n LnZ n LnZ L2nn to the current goal.

Assume H3: divides_int 2 n.

An exact proof term for the current goal is H3.

Assume H3: divides_int 2 n.

An exact proof term for the current goal is H3.

We prove the intermediate claim Ln2Z: n :/: 2 ∈ int.

An exact proof term for the current goal is divides_int_div_SNo_int 2 n L2n.

We prove the intermediate claim Ln2N: nat_p (n :/: 2).

Apply nonneg_int_nat_p (n :/: 2) Ln2Z to the current goal.

We will prove 0 ≤ n :/: 2.

Apply SNoLtLe to the current goal.

An exact proof term for the current goal is Ln2pos.

We prove the intermediate claim L1: (m :/: 2) * (m :/: 2) = 2 * (n :/: 2) * (n :/: 2).

rewrite the current goal using mul_div_SNo_both m 2 m 2 LmS SNo_2 LmS SNo_2 (from left to right).

rewrite the current goal using mul_div_SNo_both n 2 n 2 LnS SNo_2 LnS SNo_2 (from left to right).

We will prove (m * m) :/: (2 * 2) = 2 * ((n * n) :/: (2 * 2)).

rewrite the current goal using H1 (from left to right).

We will prove (2 * n * n) :/: (2 * 2) = 2 * ((n * n) :/: (2 * 2)).

Use symmetry.

An exact proof term for the current goal is mul_div_SNo_L (n * n) (2 * 2) 2 LnnS (SNo_mul_SNo 2 2 SNo_2 SNo_2) SNo_2.

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.

Apply SNoLt_irref 0 to the current goal.

We will prove 0 < 0.

rewrite the current goal using Ln20 (from right to left) at position 2.

We will prove 0 < n :/: 2.

An exact proof term for the current goal is div_SNo_pos_pos n 2 LnS SNo_2 H2 SNoLt_0_2.