Let m be given.

Assume Hm: m ∈ ω.

Let n be given.

Assume Hn: n ∈ ω ∖ 1.

Assume H1: m * m = 2 * (n * n).

Apply setminusE ω 1 n Hn to the current goal.

Assume Hn1: n ∈ ω.

Assume Hn2: n ∉ 1.

We prove the intermediate claim L1: n = 0.

An exact proof term for the current goal is form100_1_lem1 m (omega_nat_p m Hm) n (omega_nat_p n Hn1) H1.

Apply Hn2 to the current goal.

We will prove n ∈ 1.

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

We will prove 0 ∈ 1.

An exact proof term for the current goal is In_0_1.

∎