Let x be given.
Assume Hx Hxpos.
Let g be given.
Assume Hg.
Set r to be the term SNo_recipaux x g.
We prove the intermediate claim L1: ∀x' ∈ SNoS_ (SNoLev x), 0 < x' → ∀y y', SNo y → y' = (1 + (x' + - x) * y) * g x' → SNo y'.
Let x' be given.
Assume Hx' Hx'pos.
Let y and y' be given.
Assume Hy Hy'.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) x' Hx' to the current goal.
Assume _ _ Hx'1 _.
rewrite the current goal using Hy' (from left to right).
Apply SNo_mul_SNo to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is SNo_1.
Apply SNo_mul_SNo to the current goal.
Apply SNo_add_SNo to the current goal.
An exact proof term for the current goal is Hx'1.
Apply SNo_minus_SNo to the current goal.
An exact proof term for the current goal is Hx.
An exact proof term for the current goal is Hy.
Apply Hg x' Hx' Hx'pos to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim L2: ∀x' ∈ SNoS_ (SNoLev x), 0 < x' → ∀y y', SNo y → y' = (1 + (x' + - x) * y) * g x' → 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
Let x' be given.
Assume Hx' Hx'pos.
Let y and y' be given.
Assume Hy Hy'.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) x' Hx' to the current goal.
Assume _ _ Hx'1 _.
We will prove 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
Apply Hg x' Hx' Hx'pos to the current goal.
Assume Hgx'1 Hgx'2.
rewrite the current goal using mul_SNo_distrR x' (- x) (g x') Hx'1 (SNo_minus_SNo x Hx) Hgx'1 (from left to right).
We will prove 1 + - x * y' = (1 + - x * y) * (x' * g x' + (- x) * g x').
rewrite the current goal using Hgx'2 (from left to right).
We will prove 1 + - x * y' = (1 + - x * y) * (1 + (- x) * g x').
rewrite the current goal using SNo_foil 1 (- x * y) 1 ((- x) * g x') SNo_1 (SNo_minus_SNo (x * y) (SNo_mul_SNo x y Hx Hy)) SNo_1 (SNo_mul_SNo (- x) (g x') (SNo_minus_SNo x Hx) Hgx'1) (from left to right).
We will prove 1 + - x * y' = 1 * 1 + 1 * (- x) * g x' + (- x * y) * 1 + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_oneL 1 SNo_1 (from left to right).
rewrite the current goal using mul_SNo_oneL ((- x) * g x') (SNo_mul_SNo (- x) (g x') (SNo_minus_SNo x Hx) Hgx'1) (from left to right).
rewrite the current goal using mul_SNo_oneR (- x * y) (SNo_minus_SNo (x * y) (SNo_mul_SNo x y Hx Hy)) (from left to right).
We will prove 1 + - x * y' = 1 + (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
Use f_equal.
We will prove - x * y' = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using Hy' (from left to right).
We will prove - x * ((1 + (x' + - x) * y) * g x') = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_distrR 1 ((x' + - x) * y) (g x') SNo_1 (SNo_mul_SNo (x' + - x) y (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hy) Hgx'1 (from left to right).
We will prove - x * (1 * g x' + ((x' + - x) * y) * g x') = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_oneL (g x') Hgx'1 (from left to right).
We will prove - x * (g x' + ((x' + - x) * y) * g x') = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_minus_distrL x (g x' + ((x' + - x) * y) * g x') Hx (SNo_add_SNo (g x') (((x' + - x) * y) * g x') Hgx'1 (SNo_mul_SNo ((x' + - x) * y) (g x') (SNo_mul_SNo (x' + - x) y (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hy) Hgx'1)) (from right to left).
We will prove (- x) * (g x' + ((x' + - x) * y) * g x') = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_distrL (- x) (g x') (((x' + - x) * y) * g x') (SNo_minus_SNo x Hx) Hgx'1 (SNo_mul_SNo ((x' + - x) * y) (g x') (SNo_mul_SNo (x' + - x) y (SNo_add_SNo x' (- x) Hx'1 (SNo_minus_SNo x Hx)) Hy) Hgx'1) (from left to right).
We will prove (- x) * g x' + (- x) * (((x' + - x) * y) * g x') = (- x) * g x' + - x * y + (- x * y) * (- x) * g x'.
Use f_equal.
We will prove (- x) * (((x' + - x) * y) * g x') = - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_distrR x' (- x) y Hx'1 (SNo_minus_SNo x Hx) Hy (from left to right).
We will prove (- x) * ((x' * y + (- x) * y) * g x') = - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_distrR (x' * y) ((- x) * y) (g x') (SNo_mul_SNo x' y Hx'1 Hy) (SNo_mul_SNo (- x) y (SNo_minus_SNo x Hx) Hy) Hgx'1 (from left to right).
We will prove (- x) * ((x' * y) * g x' + ((- x) * y) * g x') = - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_com x' y Hx'1 Hy (from left to right).
rewrite the current goal using mul_SNo_assoc y x' (g x') Hy Hx'1 Hgx'1 (from right to left).
rewrite the current goal using Hgx'2 (from left to right).
rewrite the current goal using mul_SNo_oneR y Hy (from left to right).
We will prove (- x) * (y + ((- x) * y) * g x') = - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_distrL (- x) y (((- x) * y) * g x') (SNo_minus_SNo x Hx) Hy (SNo_mul_SNo ((- x) * y) (g x') (SNo_mul_SNo (- x) y (SNo_minus_SNo x Hx) Hy) Hgx'1) (from left to right).
We will prove (- x) * y + (- x) * ((- x) * y) * g x' = - x * y + (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_minus_distrL x y Hx Hy (from left to right) at position 1.
We will prove - x * y + (- x) * ((- x) * y) * g x' = - x * y + (- x * y) * (- x) * g x'.
Use f_equal.
We will prove (- x) * ((- x) * y) * g x' = (- x * y) * (- x) * g x'.
rewrite the current goal using mul_SNo_assoc (- x) ((- x) * y) (g x') (SNo_minus_SNo x Hx) (SNo_mul_SNo (- x) y (SNo_minus_SNo x Hx) Hy) Hgx'1 (from left to right).
rewrite the current goal using mul_SNo_assoc (- x * y) (- x) (g x') (SNo_minus_SNo (x * y) (SNo_mul_SNo x y Hx Hy)) (SNo_minus_SNo x Hx) Hgx'1 (from left to right).
Use f_equal.
We will prove (- x) * ((- x) * y) = (- x * y) * (- x).
rewrite the current goal using mul_SNo_com (- x) y (SNo_minus_SNo x Hx) Hy (from left to right).
We will prove (- x) * (y * (- x)) = (- x * y) * (- x).
rewrite the current goal using mul_SNo_minus_distrL x y Hx Hy (from right to left).
We will prove (- x) * (y * (- x)) = ((- x) * y) * (- x).
An exact proof term for the current goal is mul_SNo_assoc (- x) y (- x) (SNo_minus_SNo x Hx) Hy (SNo_minus_SNo x Hx).
Apply nat_ind to the current goal.
Apply andI to the current goal.
Let y be given.
We will prove y ∈ r 0 0 → SNo y ∧ x * y < 1.
rewrite the current goal using SNo_recipaux_0 (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove y ∈ {0} → SNo y ∧ x * y < 1.
Assume H1: y ∈ {0}.
rewrite the current goal using SingE 0 y H1 (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is SNo_0.
We will prove x * 0 < 1.
rewrite the current goal using mul_SNo_zeroR x Hx (from left to right).
An exact proof term for the current goal is SNoLt_0_1.
Let y be given.
We will prove y ∈ r 0 1 → SNo y ∧ 1 < x * y.
rewrite the current goal using SNo_recipaux_0 (from left to right).
We will prove y ∈ ({0},0) 1 → SNo y ∧ 1 < x * y.
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove y ∈ 0 → SNo y ∧ 1 < x * y.
Assume H1: y ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE y H1.
Let k be given.
Assume Hk: nat_p k.
Assume IH.
Apply IH to the current goal.
Assume IH1: ∀y ∈ r k 0, SNo y ∧ x * y < 1.
Assume IH2: ∀y ∈ r k 1, SNo y ∧ 1 < x * y.
Apply andI to the current goal.
Let y' be given.
We will prove y' ∈ r (ordsucc k) 0 → SNo y' ∧ x * y' < 1.
rewrite the current goal using SNo_recipaux_S (from left to right).
We will prove y' ∈ (r k 0 ∪ SNo_recipauxset (r k 0) x (SNoR x) g ∪ SNo_recipauxset (r k 1) x (SNoL_pos x) g,r k 1 ∪ SNo_recipauxset (r k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (r k 1) x (SNoR x) g) 0 → SNo y' ∧ x * y' < 1.
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove y' ∈ r k 0 ∪ SNo_recipauxset (r k 0) x (SNoR x) g ∪ SNo_recipauxset (r k 1) x (SNoL_pos x) g → SNo y' ∧ x * y' < 1.
Assume H1.
Apply binunionE (r k 0 ∪ SNo_recipauxset (r k 0) x (SNoR x) g) (SNo_recipauxset (r k 1) x (SNoL_pos x) g) y' H1 to the current goal.
Assume H1.
Apply binunionE (r k 0) (SNo_recipauxset (r k 0) x (SNoR x) g) y' H1 to the current goal.
An exact proof term for the current goal is IH1 y'.
Assume H1.
Apply SNo_recipauxset_E (r k 0) x (SNoR x) g y' H1 to the current goal.
Let y be given.
Assume Hy: y ∈ r k 0.
Let x' be given.
Assume Hx': x' ∈ SNoR x.
Assume H2: y' = (1 + (x' + - x) * y) * g x'.
Apply SNoR_E x Hx x' Hx' to the current goal.
Assume Hx'1 Hx'2 Hx'3.
We prove the intermediate claim Lx': x' ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 x' x Hx'1 Hx Hx'2 to the current goal.
We prove the intermediate claim Lx'pos: 0 < x'.
An exact proof term for the current goal is SNoLt_tra 0 x x' SNo_0 Hx Hx'1 Hxpos Hx'3.
Apply IH1 y Hy to the current goal.
Assume Hy1: SNo y.
Assume Hxy1: x * y < 1.
Apply Hg x' Lx' Lx'pos to the current goal.
Assume Hgx'1: SNo (g x').
Assume Hgx'2: x' * g x' = 1.
We prove the intermediate claim Ly': SNo y'.
An exact proof term for the current goal is L1 x' Lx' Lx'pos y y' Hy1 H2.
Apply andI to the current goal.
An exact proof term for the current goal is Ly'.
Apply SNo_recip_lem3 x x' (g x') y y' Hx Hxpos Hx' Hgx'1 Hgx'2 Hy1 Hxy1 Ly' to the current goal.
We will prove 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
An exact proof term for the current goal is L2 x' Lx' Lx'pos y y' Hy1 H2.
Assume H1.
Apply SNo_recipauxset_E (r k 1) x (SNoL_pos x) g y' H1 to the current goal.
Let y be given.
Assume Hy: y ∈ r k 1.
Let x' be given.
Assume Hx': x' ∈ SNoL_pos x.
Assume H2: y' = (1 + (x' + - x) * y) * g x'.
Apply SepE (SNoL x) (λw ⇒ 0 < w) x' Hx' to the current goal.
Assume Hx'0: x' ∈ SNoL x.
Assume Hx'pos: 0 < x'.
Apply SNoL_E x Hx x' Hx'0 to the current goal.
Assume Hx'1 Hx'2 Hx'3.
We prove the intermediate claim Lx': x' ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 x' x Hx'1 Hx Hx'2 to the current goal.
Apply IH2 y Hy to the current goal.
Assume Hy1: SNo y.
Assume Hxy1: 1 < x * y.
Apply Hg x' Lx' Hx'pos to the current goal.
Assume Hgx'1: SNo (g x').
Assume Hgx'2: x' * g x' = 1.
We prove the intermediate claim Ly': SNo y'.
An exact proof term for the current goal is L1 x' Lx' Hx'pos y y' Hy1 H2.
Apply andI to the current goal.
An exact proof term for the current goal is Ly'.
Apply SNo_recip_lem2 x x' (g x') y y' Hx Hxpos Hx' Hgx'1 Hgx'2 Hy1 Hxy1 Ly' to the current goal.
We will prove 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
An exact proof term for the current goal is L2 x' Lx' Hx'pos y y' Hy1 H2.
An exact proof term for the current goal is Hk.
Let y' be given.
We will prove y' ∈ r (ordsucc k) 1 → SNo y' ∧ 1 < x * y'.
rewrite the current goal using SNo_recipaux_S (from left to right).
We will prove y' ∈ (r k 0 ∪ SNo_recipauxset (r k 0) x (SNoR x) g ∪ SNo_recipauxset (r k 1) x (SNoL_pos x) g,r k 1 ∪ SNo_recipauxset (r k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (r k 1) x (SNoR x) g) 1 → SNo y' ∧ 1 < x * y'.
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove y' ∈ r k 1 ∪ SNo_recipauxset (r k 0) x (SNoL_pos x) g ∪ SNo_recipauxset (r k 1) x (SNoR x) g → SNo y' ∧ 1 < x * y'.
Assume H1.
Apply binunionE (r k 1 ∪ SNo_recipauxset (r k 0) x (SNoL_pos x) g) (SNo_recipauxset (r k 1) x (SNoR x) g) y' H1 to the current goal.
Assume H1.
Apply binunionE (r k 1) (SNo_recipauxset (r k 0) x (SNoL_pos x) g) y' H1 to the current goal.
An exact proof term for the current goal is IH2 y'.
Assume H1.
Apply SNo_recipauxset_E (r k 0) x (SNoL_pos x) g y' H1 to the current goal.
Let y be given.
Assume Hy: y ∈ r k 0.
Let x' be given.
Assume Hx': x' ∈ SNoL_pos x.
Assume H2: y' = (1 + (x' + - x) * y) * g x'.
Apply SepE (SNoL x) (λw ⇒ 0 < w) x' Hx' to the current goal.
Assume Hx'0: x' ∈ SNoL x.
Assume Hx'pos: 0 < x'.
Apply SNoL_E x Hx x' Hx'0 to the current goal.
Assume Hx'1 Hx'2 Hx'3.
We prove the intermediate claim Lx': x' ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 x' x Hx'1 Hx Hx'2 to the current goal.
Apply IH1 y Hy to the current goal.
Assume Hy1: SNo y.
Assume Hxy1: x * y < 1.
Apply Hg x' Lx' Hx'pos to the current goal.
Assume Hgx'1: SNo (g x').
Assume Hgx'2: x' * g x' = 1.
We prove the intermediate claim Ly': SNo y'.
An exact proof term for the current goal is L1 x' Lx' Hx'pos y y' Hy1 H2.
Apply andI to the current goal.
An exact proof term for the current goal is Ly'.
Apply SNo_recip_lem1 x x' (g x') y y' Hx Hxpos Hx' Hgx'1 Hgx'2 Hy1 Hxy1 Ly' to the current goal.
We will prove 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
An exact proof term for the current goal is L2 x' Lx' Hx'pos y y' Hy1 H2.
Assume H1.
Apply SNo_recipauxset_E (r k 1) x (SNoR x) g y' H1 to the current goal.
Let y be given.
Assume Hy: y ∈ r k 1.
Let x' be given.
Assume Hx': x' ∈ SNoR x.
Assume H2: y' = (1 + (x' + - x) * y) * g x'.
Apply SNoR_E x Hx x' Hx' to the current goal.
Assume Hx'1 Hx'2 Hx'3.
We prove the intermediate claim Lx': x' ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 x' x Hx'1 Hx Hx'2 to the current goal.
We prove the intermediate claim Lx'pos: 0 < x'.
An exact proof term for the current goal is SNoLt_tra 0 x x' SNo_0 Hx Hx'1 Hxpos Hx'3.
Apply IH2 y Hy to the current goal.
Assume Hy1: SNo y.
Assume Hxy1: 1 < x * y.
Apply Hg x' Lx' Lx'pos to the current goal.
Assume Hgx'1: SNo (g x').
Assume Hgx'2: x' * g x' = 1.
We prove the intermediate claim Ly': SNo y'.
An exact proof term for the current goal is L1 x' Lx' Lx'pos y y' Hy1 H2.
Apply andI to the current goal.
An exact proof term for the current goal is Ly'.
Apply SNo_recip_lem4 x x' (g x') y y' Hx Hxpos Hx' Hgx'1 Hgx'2 Hy1 Hxy1 Ly' to the current goal.
We will prove 1 + - x * y' = (1 + - x * y) * (x' + - x) * g x'.
An exact proof term for the current goal is L2 x' Lx' Lx'pos y y' Hy1 H2.
An exact proof term for the current goal is Hk.
∎