We prove the intermediate claim L1: ∀m n k, nat_p m → nat_p n → nat_p k → 2 ^ (ordsucc m) * (2 * n + 1) ≠ 2 ^ 0 * (2 * k + 1).
Let m, n and k be given.
Assume Hm Hn Hk.
Assume H1: 2 ^ (ordsucc m) * (2 * n + 1) = 2 ^ 0 * (2 * k + 1).
We prove the intermediate claim L1a: 2 ^ m ∈ ω.
We will prove 2 ^ m ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 m Hm.
We prove the intermediate claim L1b: 2 * n ∈ ω.
Apply mul_SNo_In_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_2.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is Hn.
We prove the intermediate claim L1c: 2 * n + 1 ∈ ω.
Apply add_SNo_In_omega to the current goal.
An exact proof term for the current goal is L1b.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_1.
We prove the intermediate claim L1d: 2 ^ m * (2 * n + 1) ∈ 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 L1a.
An exact proof term for the current goal is L1c.
Apply not_eq_2m_2n1 (2 ^ m * (2 * n + 1)) L1d k (Subq_omega_int k (nat_p_omega k Hk)) to the current goal.
Use transitivity with (2 * (2 ^ m)) * (2 * n + 1), 2 ^ (ordsucc m) * (2 * n + 1), and 2 ^ 0 * (2 * k + 1).
We will prove 2 * (2 ^ m * (2 * n + 1)) = (2 * (2 ^ m)) * (2 * n + 1).
An exact proof term for the current goal is mul_SNo_assoc 2 (2 ^ m) (2 * n + 1) SNo_2 (omega_SNo (2 ^ m) L1a) (omega_SNo (2 * n + 1) L1c).
We will prove (2 * (2 ^ m)) * (2 * n + 1) = 2 ^ (ordsucc m) * (2 * n + 1).
Use f_equal.
We will prove 2 * (2 ^ m) = 2 ^ (ordsucc m).
Use symmetry.
An exact proof term for the current goal is exp_SNo_nat_S 2 SNo_2 m Hm.
We will prove 2 ^ (ordsucc m) * (2 * n + 1) = 2 ^ 0 * (2 * k + 1).
An exact proof term for the current goal is H1.
We will prove 2 ^ 0 * (2 * k + 1) = 2 * k + 1.
rewrite the current goal using exp_SNo_nat_0 2 SNo_2 (from left to right).
We will prove 1 * (2 * k + 1) = 2 * k + 1.
Apply mul_SNo_oneL (2 * k + 1) to the current goal.
We will prove SNo (2 * k + 1).
Apply SNo_add_SNo to the current goal.
Apply SNo_mul_SNo to the current goal.
An exact proof term for the current goal is SNo_2.
An exact proof term for the current goal is nat_p_SNo k Hk.
An exact proof term for the current goal is SNo_1.
We prove the intermediate claim L2: ∀k, nat_p k → ∀m, nat_p m → ∀m', nat_p m' → ∀n, nat_p n → ∀n', nat_p n' → nat_pair m n = k → nat_pair m' n' = k → m = m'.
Apply nat_complete_ind to the current goal.
Let k be given.
Assume Hk.
Assume IHk: ∀k' ∈ k, ∀m, nat_p m → ∀m', nat_p m' → ∀n, nat_p n → ∀n', nat_p n' → nat_pair m n = k' → nat_pair m' n' = k' → m = m'.
Apply nat_inv_impred to the current goal.
Apply nat_inv_impred to the current goal.
Let n be given.
Assume Hn.
Let n' be given.
Assume Hn'.
Assume H1: 2 ^ 0 * (2 * n + 1) = k.
Assume H2: 2 ^ 0 * (2 * n' + 1) = k.
We will prove 0 = 0.
Use reflexivity.
Let m' be given.
Assume Hm'.
Let n be given.
Assume Hn.
Let n' be given.
Assume Hn'.
Assume H1: 2 ^ 0 * (2 * n + 1) = k.
Assume H2: 2 ^ (ordsucc m') * (2 * n' + 1) = k.
We will prove False.
We prove the intermediate claim L1a: 2 ^ m' * (2 * n' + 1) ∈ int.
Apply Subq_omega_int to the current goal.
Apply mul_SNo_In_omega to the current goal.
We will prove 2 ^ m' ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 m' Hm'.
We will prove 2 * n' + 1 ∈ ω.
Apply add_SNo_In_omega to the current goal.
Apply mul_SNo_In_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_2.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is Hn'.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_1.
Apply L1 m' n' n Hm' Hn' Hn to the current goal.
We will prove 2 ^ (ordsucc m') * (2 * n' + 1) = 2 ^ 0 * (2 * n + 1).
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is H2.
Let m be given.
Assume Hm.
Apply nat_inv_impred to the current goal.
Let n be given.
Assume Hn.
Let n' be given.
Assume Hn'.
Assume H1: 2 ^ (ordsucc m) * (2 * n + 1) = k.
Assume H2: 2 ^ 0 * (2 * n' + 1) = k.
We will prove False.
We prove the intermediate claim L1b: 2 ^ m * (2 * n + 1) ∈ int.
Apply Subq_omega_int to the current goal.
Apply mul_SNo_In_omega to the current goal.
We will prove 2 ^ m ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 m Hm.
We will prove 2 * n + 1 ∈ ω.
Apply add_SNo_In_omega to the current goal.
Apply mul_SNo_In_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_2.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is Hn.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_1.
Apply L1 m n n' Hm Hn Hn' to the current goal.
We will prove 2 ^ (ordsucc m) * (2 * n + 1) = 2 ^ 0 * (2 * n' + 1).
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is H1.
Let m' be given.
Assume Hm'.
Let n be given.
Assume Hn.
Let n' be given.
Assume Hn'.
Assume H1: 2 ^ (ordsucc m) * (2 * n + 1) = k.
Assume H2: 2 ^ (ordsucc m') * (2 * n' + 1) = k.
We will prove ordsucc m = ordsucc m'.
Use f_equal.
Set k' to be the term 2 ^ m * (2 * n + 1).
We prove the intermediate claim L2mS: SNo (2 ^ m).
An exact proof term for the current goal is SNo_exp_SNo_nat 2 SNo_2 m Hm.
We prove the intermediate claim L2m'S: SNo (2 ^ m').
An exact proof term for the current goal is SNo_exp_SNo_nat 2 SNo_2 m' Hm'.
We prove the intermediate claim L2mpos: 0 < 2 ^ m.
An exact proof term for the current goal is exp_SNo_nat_pos 2 SNo_2 SNoLt_0_2 m Hm.
We prove the intermediate claim L2SmS: SNo (2 ^ ordsucc m).
An exact proof term for the current goal is SNo_exp_SNo_nat 2 SNo_2 (ordsucc m) (nat_ordsucc m Hm).
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 (nat_p_SNo n Hn).
We prove the intermediate claim L2n1S: SNo (2 * n + 1).
An exact proof term for the current goal is SNo_add_SNo (2 * n) 1 ?? SNo_1.
We prove the intermediate claim L2n'S: SNo (2 * n').
An exact proof term for the current goal is SNo_mul_SNo 2 n' SNo_2 (nat_p_SNo n' Hn').
We prove the intermediate claim L2n'1S: SNo (2 * n' + 1).
An exact proof term for the current goal is SNo_add_SNo (2 * n') 1 ?? SNo_1.
We prove the intermediate claim L2n1pos: 0 < 2 * n + 1.
Apply SNoLeLt_tra 0 (2 * n) (2 * n + 1) SNo_0 ?? ?? to the current goal.
We will prove 0 ≤ 2 * n.
Apply mul_SNo_nonneg_nonneg 2 n SNo_2 (nat_p_SNo n Hn) to the current goal.
We will prove 0 ≤ 2.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is SNoLt_0_2.
We will prove 0 ≤ n.
An exact proof term for the current goal is omega_nonneg n (nat_p_omega n Hn).
We will prove 2 * n < 2 * n + 1.
rewrite the current goal using add_SNo_0R (2 * n) ?? (from right to left) at position 1.
We will prove 2 * n + 0 < 2 * n + 1.
An exact proof term for the current goal is add_SNo_Lt2 (2 * n) 0 1 ?? SNo_0 SNo_1 SNoLt_0_1.
We prove the intermediate claim L2: k' < k.
We will prove 2 ^ m * (2 * n + 1) < k.
rewrite the current goal using H1 (from right to left).
We will prove 2 ^ m * (2 * n + 1) < 2 ^ (ordsucc m) * (2 * n + 1).
Apply pos_mul_SNo_Lt' (2 ^ m) (2 ^ (ordsucc m)) (2 * n + 1) ?? ?? ?? ?? to the current goal.
We will prove 2 ^ m < 2 ^ (ordsucc m).
rewrite the current goal using exp_SNo_nat_S 2 SNo_2 m Hm (from left to right).
We will prove 2 ^ m < 2 * 2 ^ m.
rewrite the current goal using mul_SNo_oneL (2 ^ m) ?? (from right to left) at position 1.
We will prove 1 * 2 ^ m < 2 * 2 ^ m.
Apply pos_mul_SNo_Lt' 1 2 (2 ^ m) SNo_1 SNo_2 ?? ?? to the current goal.
We will prove 1 < 2.
An exact proof term for the current goal is SNoLt_1_2.
We prove the intermediate claim L3: k' ∈ k.
Apply ordinal_SNoLt_In k' k to the current goal.
We will prove ordinal k'.
Apply nat_p_ordinal to the current goal.
Apply omega_nat_p to the current goal.
We will prove 2 ^ m * (2 * n + 1) ∈ ω.
We will prove nat_pair m n ∈ ω.
An exact proof term for the current goal is nat_pair_In_omega m (nat_p_omega m Hm) n (nat_p_omega n Hn).
We will prove ordinal k.
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is Hk.
We will prove k' < k.
An exact proof term for the current goal is L2.
We prove the intermediate claim L4: 2 ^ m * (2 * n + 1) = k'.
Use reflexivity.
We prove the intermediate claim L5: 2 ^ m' * (2 * n' + 1) = k'.
We will prove 2 ^ m' * (2 * n' + 1) = 2 ^ m * (2 * n + 1).
Apply mul_SNo_nonzero_cancel_L 2 (2 ^ m' * (2 * n' + 1)) (2 ^ m * (2 * n + 1)) SNo_2 neq_2_0 (SNo_mul_SNo (2 ^ m') (2 * n' + 1) ?? ??) (SNo_mul_SNo (2 ^ m) (2 * n + 1) ?? ??) to the current goal.
We will prove 2 * (2 ^ m' * (2 * n' + 1)) = 2 * (2 ^ m * (2 * n + 1)).
Use transitivity with (2 * (2 ^ m')) * (2 * n' + 1), (2 ^ (ordsucc m')) * (2 * n' + 1), k, (2 ^ (ordsucc m)) * (2 * n + 1), and (2 * (2 ^ m)) * (2 * n + 1).
An exact proof term for the current goal is mul_SNo_assoc 2 (2 ^ m') (2 * n' + 1) SNo_2 ?? ??.
Use f_equal.
Use symmetry.
An exact proof term for the current goal is exp_SNo_nat_S 2 SNo_2 m' Hm'.
An exact proof term for the current goal is H2.
Use symmetry.
An exact proof term for the current goal is H1.
Use f_equal.
An exact proof term for the current goal is exp_SNo_nat_S 2 SNo_2 m Hm.
Use symmetry.
An exact proof term for the current goal is mul_SNo_assoc 2 (2 ^ m) (2 * n + 1) SNo_2 ?? ??.
We will prove m = m'.
An exact proof term for the current goal is IHk k' L3 m Hm m' Hm' n Hn n' Hn' L4 L5.
Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
Let m' be given.
Assume Hm'.
Let n' be given.
Assume Hn'.
Assume H1: nat_pair m n = nat_pair m' n'.
Apply L2 (nat_pair m' n') (omega_nat_p (nat_pair m' n') (nat_pair_In_omega m' Hm' n' Hn')) m (omega_nat_p m Hm) m' (omega_nat_p m' Hm') n (omega_nat_p n Hn) n' (omega_nat_p n' Hn') to the current goal.
We will prove nat_pair m n = nat_pair m' n'.
An exact proof term for the current goal is H1.
We will prove nat_pair m' n' = nat_pair m' n'.
Use reflexivity.
∎