Let m be given.
Assume Hm: m ∈ int.
Let n be given.
Assume Hn: n ∈ int.
Assume H1: 2 * m = 2 * n + 1.
Apply prime_not_divides_int_1 2 prime_nat_2 to the current goal.
We will prove divides_int 2 1.
We prove the intermediate claim LmS: SNo m.
An exact proof term for the current goal is int_SNo m Hm.
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is int_SNo n Hn.
We prove the intermediate claim L2nS: SNo (2 * n).
An exact proof term for the current goal is SNo_mul_SNo 2 n SNo_2 LnS.
We prove the intermediate claim L2mS: SNo (2 * m).
An exact proof term for the current goal is SNo_mul_SNo 2 m SNo_2 LmS.
We prove the intermediate claim Lm2nS: SNo (- 2 * n).
An exact proof term for the current goal is SNo_minus_SNo (2 * n) L2nS.
We prove the intermediate claim L1: 2 * n + 2 * m + - 2 * n = 2 * n + 1.
rewrite the current goal using H1 (from right to left).
We will prove 2 * n + 2 * m + - 2 * n = 2 * m.
rewrite the current goal using add_SNo_rotate_3_1 (2 * n) (2 * m) (- 2 * n) L2nS L2mS Lm2nS (from left to right).
We will prove - 2 * n + 2 * n + 2 * m = 2 * m.
An exact proof term for the current goal is add_SNo_minus_L2 (2 * n) (2 * m) L2nS L2mS.
We prove the intermediate claim L2: 2 * (m + - n) = 1.
rewrite the current goal using mul_SNo_distrL 2 m (- n) SNo_2 LmS (SNo_minus_SNo n LnS) (from left to right).
rewrite the current goal using mul_SNo_minus_distrR 2 n SNo_2 LnS (from left to right).
We will prove 2 * m + - 2 * n = 1.
An exact proof term for the current goal is add_SNo_cancel_L (2 * n) (2 * m + - 2 * n) 1 L2nS (SNo_add_SNo (2 * m) (- 2 * n) L2mS Lm2nS) SNo_1 L1.
rewrite the current goal using L2 (from right to left) at position 2.
We will prove divides_int 2 (2 * (m + - n)).
Apply divides_int_mul_SNo_L 2 2 (m + - n) (int_add_SNo m Hm (- n) (int_minus_SNo n Hn)) to the current goal.
We will prove divides_int 2 2.
Apply divides_int_ref 2 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.
∎