Let a be given.
Assume Ha.
Let b be given.
Assume Hb.
Assume H1: ¬ (a = 0 b = 0).
We prove the intermediate claim LaS: SNo a.
An exact proof term for the current goal is int_SNo a Ha.
We prove the intermediate claim LbS: SNo b.
An exact proof term for the current goal is int_SNo b Hb.
Set p to be the term λc ⇒ int_lin_comb a b c 0 < c of type setprop.
We prove the intermediate claim L1: c, ordinal c p c.
Apply int_3_cases a Ha to the current goal.
Let a' be given.
Assume Ha': a' ω.
Assume Haa': a = - ordsucc a'.
We prove the intermediate claim La'N: nat_p a'.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Ha'.
We prove the intermediate claim La': ordinal a'.
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is La'N.
We prove the intermediate claim LSa'S: SNo (ordsucc a').
Apply nat_p_SNo to the current goal.
Apply nat_ordsucc to the current goal.
An exact proof term for the current goal is La'N.
We use ordsucc a' to witness the existential quantifier.
Apply andI to the current goal.
We will prove ordinal (ordsucc a').
Apply ordinal_ordsucc to the current goal.
An exact proof term for the current goal is La'.
We will prove int_lin_comb a b (ordsucc a') 0 < ordsucc a'.
Apply andI to the current goal.
We will prove int_lin_comb a b (ordsucc a').
Apply int_lin_comb_I to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
We will prove ordsucc a' int.
Apply Subq_omega_int to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Ha'.
We will prove m nint, m * a + n * b = ordsucc a'.
We use (- 1) to witness the existential quantifier.
Apply andI to the current goal.
We will prove - 1 int.
Apply int_minus_SNo_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_1.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 0 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_0.
We will prove (- 1) * a + 0 * b = ordsucc a'.
rewrite the current goal using mul_SNo_zeroL b LbS (from left to right).
We will prove (- 1) * a + 0 = ordsucc a'.
rewrite the current goal using mul_SNo_minus_distrL 1 a SNo_1 LaS (from left to right).
We will prove - 1 * a + 0 = ordsucc a'.
rewrite the current goal using mul_SNo_oneL a LaS (from left to right).
We will prove - a + 0 = ordsucc a'.
rewrite the current goal using Haa' (from left to right).
We will prove - - ordsucc a' + 0 = ordsucc a'.
rewrite the current goal using minus_SNo_invol (ordsucc a') LSa'S (from left to right).
An exact proof term for the current goal is add_SNo_0R (ordsucc a') LSa'S.
We will prove 0 < ordsucc a'.
An exact proof term for the current goal is ordinal_ordsucc_pos a' La'.
Assume H2: a = 0.
Apply int_3_cases b Hb to the current goal.
Let b' be given.
Assume Hb': b' ω.
Assume Hbb': b = - ordsucc b'.
We prove the intermediate claim Lb'N: nat_p b'.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hb'.
We prove the intermediate claim Lb': ordinal b'.
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is Lb'N.
We prove the intermediate claim LSb'S: SNo (ordsucc b').
Apply nat_p_SNo to the current goal.
Apply nat_ordsucc to the current goal.
An exact proof term for the current goal is Lb'N.
We use ordsucc b' to witness the existential quantifier.
Apply andI to the current goal.
We will prove ordinal (ordsucc b').
Apply ordinal_ordsucc to the current goal.
An exact proof term for the current goal is Lb'.
We will prove int_lin_comb a b (ordsucc b') 0 < ordsucc b'.
Apply andI to the current goal.
We will prove int_lin_comb a b (ordsucc b').
Apply int_lin_comb_I to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
We will prove ordsucc b' int.
Apply Subq_omega_int to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hb'.
We will prove m nint, m * a + n * b = ordsucc b'.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 0 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_0.
We use (- 1) to witness the existential quantifier.
Apply andI to the current goal.
We will prove - 1 int.
Apply int_minus_SNo_omega to the current goal.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_1.
We will prove 0 * a + (- 1) * b = ordsucc b'.
rewrite the current goal using mul_SNo_zeroL a LaS (from left to right).
We will prove 0 + (- 1) * b = ordsucc b'.
rewrite the current goal using mul_SNo_minus_distrL 1 b SNo_1 LbS (from left to right).
We will prove 0 + - 1 * b = ordsucc b'.
rewrite the current goal using mul_SNo_oneL b LbS (from left to right).
We will prove 0 + - b = ordsucc b'.
rewrite the current goal using Hbb' (from left to right).
We will prove 0 + - - ordsucc b' = ordsucc b'.
rewrite the current goal using minus_SNo_invol (ordsucc b') LSb'S (from left to right).
An exact proof term for the current goal is add_SNo_0L (ordsucc b') LSb'S.
We will prove 0 < ordsucc b'.
An exact proof term for the current goal is ordinal_ordsucc_pos b' Lb'.
Assume H3: b = 0.
We will prove False.
Apply H1 to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H3.
Let b' be given.
Assume Hb': b' ω.
Assume Hbb': b = ordsucc b'.
We prove the intermediate claim Lb': ordinal b'.
Apply nat_p_ordinal to the current goal.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hb'.
We use ordsucc b' to witness the existential quantifier.
Apply andI to the current goal.
We will prove ordinal (ordsucc b').
Apply ordinal_ordsucc to the current goal.
An exact proof term for the current goal is Lb'.
We will prove int_lin_comb a b (ordsucc b') 0 < ordsucc b'.
Apply andI to the current goal.
We will prove int_lin_comb a b (ordsucc b').
Apply int_lin_comb_I to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
We will prove ordsucc b' int.
Apply Subq_omega_int to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hb'.
We will prove m nint, m * a + n * b = ordsucc b'.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 0 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_0.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 1 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_1.
We will prove 0 * a + 1 * b = ordsucc b'.
rewrite the current goal using Hbb' (from right to left).
rewrite the current goal using mul_SNo_zeroL a LaS (from left to right).
rewrite the current goal using mul_SNo_oneL b LbS (from left to right).
We will prove 0 + b = b.
An exact proof term for the current goal is add_SNo_0L b LbS.
We will prove 0 < ordsucc b'.
An exact proof term for the current goal is ordinal_ordsucc_pos b' Lb'.
Let a' be given.
Assume Ha': a' ω.
Assume Haa': a = ordsucc a'.
We prove the intermediate claim La': ordinal a'.
Apply nat_p_ordinal to the current goal.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Ha'.
We use ordsucc a' to witness the existential quantifier.
Apply andI to the current goal.
We will prove ordinal (ordsucc a').
Apply ordinal_ordsucc to the current goal.
An exact proof term for the current goal is La'.
We will prove int_lin_comb a b (ordsucc a') 0 < ordsucc a'.
Apply andI to the current goal.
We will prove int_lin_comb a b (ordsucc a').
Apply int_lin_comb_I to the current goal.
An exact proof term for the current goal is Ha.
An exact proof term for the current goal is Hb.
We will prove ordsucc a' int.
Apply Subq_omega_int to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Ha'.
We will prove m nint, m * a + n * b = ordsucc a'.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 1 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_1.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 0 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_0.
We will prove 1 * a + 0 * b = ordsucc a'.
rewrite the current goal using Haa' (from right to left).
rewrite the current goal using mul_SNo_zeroL b LbS (from left to right).
rewrite the current goal using mul_SNo_oneL a LaS (from left to right).
We will prove a + 0 = a.
An exact proof term for the current goal is add_SNo_0R a LaS.
We will prove 0 < ordsucc a'.
An exact proof term for the current goal is ordinal_ordsucc_pos a' La'.
We prove the intermediate claim L2: c, ordinal c p c βc, ¬ p β.
An exact proof term for the current goal is least_ordinal_ex p L1.
Apply L2 to the current goal.
Let c be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hco: ordinal c.
Assume Hc1: int_lin_comb a b c 0 < c.
Assume Hc2: βc, ¬ p β.
We prove the intermediate claim LcS: SNo c.
An exact proof term for the current goal is ordinal_SNo c Hco.
We use c to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hc1.
Let c' be given.
Assume Hc'1: int_lin_comb a b c'.
Assume Hc'2: 0 < c'.
We will prove c c'.
We prove the intermediate claim Lc'Z: c' int.
An exact proof term for the current goal is int_lin_comb_E3 a b c' Hc'1.
We prove the intermediate claim Lc'S: SNo c'.
An exact proof term for the current goal is int_SNo c' Lc'Z.
Apply SNoLtLe_or c' c Lc'S LcS to the current goal.
Assume H2: c' < c.
We will prove False.
We prove the intermediate claim Lc'N: nat_p c'.
Apply nonneg_int_nat_p c' Lc'Z to the current goal.
We will prove 0 c'.
Apply SNoLtLe to the current goal.
We will prove 0 < c'.
An exact proof term for the current goal is Hc'2.
We prove the intermediate claim L3: c' c.
An exact proof term for the current goal is ordinal_SNoLt_In c' c (nat_p_ordinal c' Lc'N) Hco H2.
Apply Hc2 c' L3 to the current goal.
We will prove p c'.
We will prove int_lin_comb a b c' 0 < c'.
Apply andI to the current goal.
An exact proof term for the current goal is Hc'1.
An exact proof term for the current goal is Hc'2.
Assume H2: c c'.
An exact proof term for the current goal is H2.