Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), 0 < w → SNo (recip_SNo_pos w) ∧ w * recip_SNo_pos w = 1.
Assume Hxpos: 0 < x.
We will prove SNo (recip_SNo_pos x) ∧ x * recip_SNo_pos x = 1.
rewrite the current goal using recip_SNo_pos_eq x Hx (from left to right).
We will prove SNo (G x recip_SNo_pos) ∧ x * G x recip_SNo_pos = 1.
Set L to be the term ⋃k ∈ ωSNo_recipaux x recip_SNo_pos k 0.
Set R to be the term ⋃k ∈ ωSNo_recipaux x recip_SNo_pos k 1.
We prove the intermediate claim L1: ∀k, nat_p k → (∀y ∈ SNo_recipaux x recip_SNo_pos k 0, SNo y ∧ x * y < 1) ∧ (∀y ∈ SNo_recipaux x recip_SNo_pos k 1, SNo y ∧ 1 < x * y).
An exact proof term for the current goal is SNo_recipaux_lem1 x Hx Hxpos recip_SNo_pos IH.
We prove the intermediate claim L1L: ∀w ∈ L, x * w < 1.
Let w be given.
Assume Hw.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) w Hw to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: w ∈ SNo_recipaux x recip_SNo_pos k 0.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume H2 _.
Apply H2 w H1 to the current goal.
Assume _ H3.
An exact proof term for the current goal is H3.
We prove the intermediate claim L1R: ∀z ∈ R, 1 < x * z.
Let z be given.
Assume Hz.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) z Hz to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H1: z ∈ SNo_recipaux x recip_SNo_pos k 1.
Apply L1 k (omega_nat_p k Hk) to the current goal.
Assume _ H2.
Apply H2 z H1 to the current goal.
Assume _ H3.
An exact proof term for the current goal is H3.
We prove the intermediate claim L2: SNoCutP L R.
An exact proof term for the current goal is SNo_recipaux_lem2 x Hx Hxpos recip_SNo_pos IH.
Apply L2 to the current goal.
Assume HLHR.
Apply HLHR to the current goal.
Assume HL: ∀w ∈ L, SNo w.
Assume HR: ∀z ∈ R, SNo z.
Assume HLR: ∀w ∈ L, ∀z ∈ R, w < z.
Set y to be the term SNoCut L R.
Apply SNoCutP_SNoCut_impred L R L2 to the current goal.
Assume H1: SNo y.
Assume H2: SNoLev y ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume H3: ∀w ∈ L, w < y.
Assume H4: ∀z ∈ R, y < z.
Assume H5: ∀u, SNo u → (∀w ∈ L, w < u) → (∀z ∈ R, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u.
We prove the intermediate claim L3: SNo (x * y).
An exact proof term for the current goal is SNo_mul_SNo x y Hx H1.
We prove the intermediate claim L4: 0 < y.
Apply H3 to the current goal.
We will prove 0 ∈ L.
Apply famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) 0 to the current goal.
We will prove 0 ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_0.
We will prove 0 ∈ SNo_recipaux x recip_SNo_pos 0 0.
rewrite the current goal using SNo_recipaux_0 (from left to right).
We will prove 0 ∈ ({0},0) 0.
rewrite the current goal using tuple_2_0_eq (from left to right).
Apply SingI to the current goal.
We prove the intermediate claim L5: 0 < x * y.
An exact proof term for the current goal is mul_SNo_pos_pos x y Hx H1 Hxpos L4.
We prove the intermediate claim L6: ∀w ∈ SNoL y, ∃w' ∈ L, w ≤ w'.
An exact proof term for the current goal is SNoL_SNoCutP_ex L R L2.
We prove the intermediate claim L7: ∀z ∈ SNoR y, ∃z' ∈ R, z' ≤ z.
An exact proof term for the current goal is SNoR_SNoCutP_ex L R L2.
Apply andI to the current goal.
We will prove SNo y.
An exact proof term for the current goal is H1.
We will prove x * y = 1.
Apply dneg to the current goal.
Assume HC: x * y ≠ 1.
Apply SNoLt_trichotomy_or_impred (x * y) 1 L3 SNo_1 to the current goal.
Assume H6: x * y < 1.
We prove the intermediate claim L8: 1 ∈ SNoR (x * y).
Apply SNoR_I to the current goal.
An exact proof term for the current goal is L3.
An exact proof term for the current goal is SNo_1.
We will prove SNoLev 1 ∈ SNoLev (x * y).
rewrite the current goal using ordinal_SNoLev 1 ordinal_1 (from left to right).
We will prove 1 ∈ SNoLev (x * y).
Apply ordinal_In_Or_Subq 1 (SNoLev (x * y)) ordinal_1 (SNoLev_ordinal (x * y) L3) to the current goal.
Assume H7: 1 ∈ SNoLev (x * y).
An exact proof term for the current goal is H7.
Assume H7: SNoLev (x * y) ⊆ 1.
We will prove False.
Apply HC to the current goal.
We will prove x * y = 1.
An exact proof term for the current goal is pos_low_eq_one (x * y) L3 L5 H7.
An exact proof term for the current goal is H6.
We prove the intermediate claim L9: ∀v w w', SNo v → SNo w → SNo w' → v ∈ SNoS_ (SNoLev x) → 0 < v → v * y + x * w ≤ 1 + v * w → (1 + (v + - x) * w') * recip_SNo_pos v ∈ L → (- v + x) * w' ≤ (- v + x) * w → False.
Let v, w and w' be given.
Assume Hv1 Hw1 Hw' HvS Hvpos H7 Hw'' H8.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw''1: SNo w''.
An exact proof term for the current goal is HL w'' Hw''.
Apply SNoLt_irref 1 to the current goal.
We will prove 1 < 1.
Apply SNoLtLe_tra 1 (1 + v * (y + - w'')) 1 SNo_1 (SNo_add_SNo 1 (v * (y + - w'')) SNo_1 (SNo_mul_SNo v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1)))) SNo_1 to the current goal.
We will prove 1 < 1 + v * (y + - w'').
rewrite the current goal using add_SNo_0R 1 SNo_1 (from right to left) at position 1.
We will prove 1 + 0 < 1 + v * (y + - w'').
Apply add_SNo_Lt2 1 0 (v * (y + - w'')) SNo_1 SNo_0 (SNo_mul_SNo v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1))) to the current goal.
We will prove 0 < v * (y + - w'').
Apply mul_SNo_pos_pos v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1)) Hvpos to the current goal.
We will prove 0 < y + - w''.
Apply SNoLt_minus_pos w'' y Lw''1 H1 to the current goal.
We will prove w'' < y.
An exact proof term for the current goal is H3 w'' Hw''.
We will prove 1 + v * (y + - w'') ≤ 1.
rewrite the current goal using mul_SNo_distrL v y (- w'') Hv1 H1 (SNo_minus_SNo w'' Lw''1) (from left to right).
We will prove 1 + v * y + v * (- w'') ≤ 1.
rewrite the current goal using mul_SNo_minus_distrR v w'' Hv1 Lw''1 (from left to right).
We will prove 1 + v * y + - v * w'' ≤ 1.
We will prove 1 + v * y + - v * (1 + (v + - x) * w') * recip_SNo_pos v ≤ 1.
Apply IH v HvS Hvpos to the current goal.
Assume Hrv1: SNo (recip_SNo_pos v).
Assume Hrv2: v * recip_SNo_pos v = 1.
rewrite the current goal using mul_SNo_com (1 + (v + - x) * w') (recip_SNo_pos v) (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) Hrv1 (from left to right).
We will prove 1 + v * y + - v * recip_SNo_pos v * (1 + (v + - x) * w') ≤ 1.
rewrite the current goal using mul_SNo_assoc v (recip_SNo_pos v) (1 + (v + - x) * w') Hv1 Hrv1 (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (from left to right).
We will prove 1 + v * y + - (v * recip_SNo_pos v) * (1 + (v + - x) * w') ≤ 1.
rewrite the current goal using Hrv2 (from left to right).
We will prove 1 + v * y + - 1 * (1 + (v + - x) * w') ≤ 1.
rewrite the current goal using mul_SNo_oneL (1 + (v + - x) * w') (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (from left to right).
We will prove 1 + v * y + - (1 + (v + - x) * w') ≤ 1.
rewrite the current goal using minus_add_SNo_distr 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw') (from left to right).
We will prove 1 + v * y + - 1 + - (v + - x) * w' ≤ 1.
rewrite the current goal using add_SNo_rotate_3_1 (- 1) (- (v + - x) * w') (v * y) (SNo_minus_SNo 1 SNo_1) (SNo_minus_SNo ((v + - x) * w') (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (SNo_mul_SNo v y Hv1 H1) (from right to left).
We will prove 1 + - 1 + - (v + - x) * w' + v * y ≤ 1.
rewrite the current goal using add_SNo_minus_SNo_prop2 1 (- (v + - x) * w' + v * y) SNo_1 (SNo_add_SNo (- (v + - x) * w') (v * y) (SNo_minus_SNo ((v + - x) * w') (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (SNo_mul_SNo v y Hv1 H1)) (from left to right).
We will prove - (v + - x) * w' + v * y ≤ 1.
rewrite the current goal using mul_SNo_minus_distrL (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw' (from right to left).
We will prove (- (v + - x)) * w' + v * y ≤ 1.
rewrite the current goal using minus_add_SNo_distr v (- x) Hv1 (SNo_minus_SNo x Hx) (from left to right).
rewrite the current goal using minus_SNo_invol x Hx (from left to right).
We will prove (- v + x) * w' + v * y ≤ 1.
Apply SNoLe_tra ((- v + x) * w' + v * y) ((- v + x) * w + v * y) 1 (SNo_add_SNo ((- v + x) * w') (v * y) (SNo_mul_SNo (- v + x) w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw') (SNo_mul_SNo v y Hv1 H1)) (SNo_add_SNo ((- v + x) * w) (v * y) (SNo_mul_SNo (- v + x) w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw1) (SNo_mul_SNo v y Hv1 H1)) SNo_1 to the current goal.
We will prove (- v + x) * w' + v * y ≤ (- v + x) * w + v * y.
Apply add_SNo_Le1 ((- v + x) * w') (v * y) ((- v + x) * w) (SNo_mul_SNo (- v + x) w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw') (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo (- v + x) w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw1) to the current goal.
We will prove (- v + x) * w' ≤ (- v + x) * w.
An exact proof term for the current goal is H8.
We will prove (- v + x) * w + v * y ≤ 1.
rewrite the current goal using mul_SNo_distrR (- v) x w (SNo_minus_SNo v Hv1) Hx Hw1 (from left to right).
We will prove ((- v) * w + x * w) + v * y ≤ 1.
rewrite the current goal using mul_SNo_minus_distrL v w Hv1 Hw1 (from left to right).
We will prove (- v * w + x * w) + v * y ≤ 1.
rewrite the current goal using add_SNo_assoc (- v * w) (x * w) (v * y) (SNo_minus_SNo (v * w) (SNo_mul_SNo v w Hv1 Hw1)) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1) (from right to left).
We will prove - v * w + x * w + v * y ≤ 1.
rewrite the current goal using add_SNo_com (- v * w) (x * w + v * y) (SNo_minus_SNo (v * w) (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1)) (from left to right).
Apply add_SNo_minus_Le2 1 (- v * w) (x * w + v * y) SNo_1 (SNo_minus_SNo (v * w) (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1)) to the current goal.
We will prove x * w + v * y ≤ 1 + - - v * w.
rewrite the current goal using minus_SNo_invol (v * w) (SNo_mul_SNo v w Hv1 Hw1) (from left to right).
We will prove x * w + v * y ≤ 1 + v * w.
rewrite the current goal using add_SNo_com (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1) (from left to right).
We will prove v * y + x * w ≤ 1 + v * w.
An exact proof term for the current goal is H7.
Apply mul_SNo_SNoR_interpolate_impred x y Hx H1 1 L8 to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Let w be given.
Assume Hw: w ∈ SNoR y.
Assume H7: v * y + x * w ≤ 1 + v * w.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
Apply SNoR_E y H1 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: y < w.
We prove the intermediate claim LvS: v ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 v x Hv1 Hx Hv2.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
Apply L7 w Hw to the current goal.
Let w' be given.
Assume Hw'.
Apply Hw' to the current goal.
Assume Hw'1: w' ∈ R.
Assume Hw'2: w' ≤ w.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HR w' Hw'1.
We prove the intermediate claim Lxw': SNo (x * w').
An exact proof term for the current goal is SNo_mul_SNo x w' Hx Lw'.
We prove the intermediate claim Lvpos: 0 < v.
Apply SNoLtLe_or 0 v SNo_0 Hv1 to the current goal.
Assume H8: 0 < v.
An exact proof term for the current goal is H8.
Assume H8: v ≤ 0.
We will prove False.
Apply SNoLt_irref 1 to the current goal.
We will prove 1 < 1.
Apply SNoLtLe_tra 1 (x * w') 1 SNo_1 Lxw' SNo_1 to the current goal.
We will prove 1 < x * w'.
An exact proof term for the current goal is L1R w' Hw'1.
We will prove x * w' ≤ 1.
Apply SNoLe_tra (x * w') (x * w) 1 Lxw' Lxw SNo_1 to the current goal.
We will prove x * w' ≤ x * w.
An exact proof term for the current goal is nonneg_mul_SNo_Le x w' w Hx (SNoLtLe 0 x Hxpos) Lw' Hw1 Hw'2.
We will prove x * w ≤ 1.
Apply SNoLe_tra (x * w) (v * (y + - w) + x * w) 1 Lxw (SNo_add_SNo (v * (y + - w)) (x * w) (SNo_mul_SNo v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1))) Lxw) SNo_1 to the current goal.
We will prove x * w ≤ v * (y + - w) + x * w.
rewrite the current goal using add_SNo_0L (x * w) Lxw (from right to left) at position 1.
We will prove 0 + x * w ≤ v * (y + - w) + x * w.
Apply add_SNo_Le1 0 (x * w) (v * (y + - w)) SNo_0 Lxw (SNo_mul_SNo v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1))) to the current goal.
We will prove 0 ≤ v * (y + - w).
Apply mul_SNo_nonpos_neg v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1)) H8 to the current goal.
We will prove y + - w < 0.
Apply add_SNo_minus_Lt1b y w 0 H1 Hw1 SNo_0 to the current goal.
We will prove y < 0 + w.
rewrite the current goal using add_SNo_0L w Hw1 (from left to right).
We will prove y < w.
An exact proof term for the current goal is Hw3.
We will prove v * (y + - w) + x * w ≤ 1.
rewrite the current goal using mul_SNo_distrL v y (- w) Hv1 H1 (SNo_minus_SNo w Hw1) (from left to right).
We will prove (v * y + v * (- w)) + x * w ≤ 1.
rewrite the current goal using add_SNo_com_3b_1_2 (v * y) (v * (- w)) (x * w) (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo v (- w) Hv1 (SNo_minus_SNo w Hw1)) Lxw (from left to right).
We will prove (v * y + x * w) + v * (- w) ≤ 1.
Apply add_SNo_minus_Le2 1 (v * (- w)) (v * y + x * w) SNo_1 (SNo_mul_SNo v (- w) Hv1 (SNo_minus_SNo w Hw1)) (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Hv1 H1) Lxw) to the current goal.
We will prove v * y + x * w ≤ 1 + - v * (- w).
rewrite the current goal using mul_SNo_minus_distrR v w Hv1 Hw1 (from left to right).
rewrite the current goal using minus_SNo_invol (v * w) (SNo_mul_SNo v w Hv1 Hw1) (from left to right).
An exact proof term for the current goal is H7.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw'': w'' ∈ L.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) w' Hw'1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H9: w' ∈ SNo_recipaux x recip_SNo_pos k 1.
Apply famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) (ordsucc k) w'' (omega_ordsucc k Hk) to the current goal.
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos (ordsucc k) 0.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos k 0 ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos.
Apply binunionI2 to the current goal.
We will prove w'' ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos.
Apply SNo_recipauxset_I (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos to the current goal.
We will prove w' ∈ SNo_recipaux x recip_SNo_pos k 1.
An exact proof term for the current goal is H9.
We will prove v ∈ SNoL_pos x.
We will prove v ∈ {w ∈ SNoL x|0 < w}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hv.
We will prove 0 < v.
An exact proof term for the current goal is Lvpos.
Apply L9 v w w' Hv1 Hw1 Lw' LvS Lvpos H7 Lw'' to the current goal.
We will prove (- v + x) * w' ≤ (- v + x) * w.
Apply nonneg_mul_SNo_Le (- v + x) w' w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) to the current goal.
We will prove 0 ≤ - v + x.
rewrite the current goal using add_SNo_com (- v) x (SNo_minus_SNo v Hv1) Hx (from left to right).
We will prove 0 ≤ x + - v.
Apply add_SNo_minus_Le2b x v 0 Hx Hv1 SNo_0 to the current goal.
We will prove 0 + v ≤ x.
rewrite the current goal using add_SNo_0L v Hv1 (from left to right).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hv3.
An exact proof term for the current goal is Lw'.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Hw'2.
Let v be given.
Assume Hv: v ∈ SNoR x.
Let w be given.
Assume Hw: w ∈ SNoL y.
Assume H7: v * y + x * w ≤ 1 + v * w.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: x < v.
Apply SNoL_E y H1 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: w < y.
We prove the intermediate claim LvS: v ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 v x Hv1 Hx Hv2.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
Apply L6 w Hw to the current goal.
Let w' be given.
Assume Hw'.
Apply Hw' to the current goal.
Assume Hw'1: w' ∈ L.
Assume Hw'2: w ≤ w'.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HL w' Hw'1.
We prove the intermediate claim Lxw': SNo (x * w').
An exact proof term for the current goal is SNo_mul_SNo x w' Hx Lw'.
We prove the intermediate claim Lvpos: 0 < v.
An exact proof term for the current goal is SNoLt_tra 0 x v SNo_0 Hx Hv1 Hxpos Hv3.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw'': w'' ∈ L.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) w' Hw'1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H9: w' ∈ SNo_recipaux x recip_SNo_pos k 0.
Apply famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) (ordsucc k) w'' (omega_ordsucc k Hk) to the current goal.
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos (ordsucc k) 0.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos k 0 ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoL_pos x) recip_SNo_pos.
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
We will prove w'' ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos.
Apply SNo_recipauxset_I (SNo_recipaux x recip_SNo_pos k 0) x (SNoR x) recip_SNo_pos to the current goal.
We will prove w' ∈ SNo_recipaux x recip_SNo_pos k 0.
An exact proof term for the current goal is H9.
We will prove v ∈ SNoR x.
An exact proof term for the current goal is Hv.
Apply L9 v w w' Hv1 Hw1 Lw' LvS Lvpos H7 Lw'' to the current goal.
We will prove (- v + x) * w' ≤ (- v + x) * w.
Apply nonpos_mul_SNo_Le (- v + x) w' w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) to the current goal.
We will prove - v + x ≤ 0.
rewrite the current goal using add_SNo_com (- v) x (SNo_minus_SNo v Hv1) Hx (from left to right).
We will prove x + - v ≤ 0.
Apply add_SNo_minus_Le2 0 (- v) x SNo_0 (SNo_minus_SNo v Hv1) Hx to the current goal.
rewrite the current goal using minus_SNo_invol v Hv1 (from left to right).
We will prove x ≤ 0 + v.
rewrite the current goal using add_SNo_0L v Hv1 (from left to right).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hv3.
An exact proof term for the current goal is Lw'.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Hw'2.
Assume H6: x * y = 1.
Apply HC to the current goal.
An exact proof term for the current goal is H6.
Assume H6: 1 < x * y.
We prove the intermediate claim L10: 1 ∈ SNoL (x * y).
Apply SNoL_I to the current goal.
An exact proof term for the current goal is L3.
An exact proof term for the current goal is SNo_1.
We will prove SNoLev 1 ∈ SNoLev (x * y).
rewrite the current goal using ordinal_SNoLev 1 ordinal_1 (from left to right).
We will prove 1 ∈ SNoLev (x * y).
Apply ordinal_In_Or_Subq 1 (SNoLev (x * y)) ordinal_1 (SNoLev_ordinal (x * y) L3) to the current goal.
Assume H7: 1 ∈ SNoLev (x * y).
An exact proof term for the current goal is H7.
Assume H7: SNoLev (x * y) ⊆ 1.
We will prove False.
Apply HC to the current goal.
We will prove x * y = 1.
An exact proof term for the current goal is pos_low_eq_one (x * y) L3 L5 H7.
An exact proof term for the current goal is H6.
We prove the intermediate claim L11: ∀v w w', SNo v → SNo w → SNo w' → v ∈ SNoS_ (SNoLev x) → 0 < v → 1 + v * w ≤ v * y + x * w → (1 + (v + - x) * w') * recip_SNo_pos v ∈ R → (- v + x) * w ≤ (- v + x) * w' → False.
Let v, w and w' be given.
Assume Hv1 Hw1 Hw' HvS Hvpos H7 Hw'' H8.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw''1: SNo w''.
An exact proof term for the current goal is HR w'' Hw''.
Apply SNoLt_irref 1 to the current goal.
We will prove 1 < 1.
Apply SNoLeLt_tra 1 (1 + v * (y + - w'')) 1 SNo_1 (SNo_add_SNo 1 (v * (y + - w'')) SNo_1 (SNo_mul_SNo v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1)))) SNo_1 to the current goal.
We will prove 1 ≤ 1 + v * (y + - w'').
rewrite the current goal using mul_SNo_distrL v y (- w'') Hv1 H1 (SNo_minus_SNo w'' Lw''1) (from left to right).
We will prove 1 ≤ 1 + v * y + v * (- w'').
rewrite the current goal using mul_SNo_minus_distrR v w'' Hv1 Lw''1 (from left to right).
We will prove 1 ≤ 1 + v * y + - v * w''.
We will prove 1 ≤ 1 + v * y + - v * (1 + (v + - x) * w') * recip_SNo_pos v.
Apply IH v HvS Hvpos to the current goal.
Assume Hrv1: SNo (recip_SNo_pos v).
Assume Hrv2: v * recip_SNo_pos v = 1.
rewrite the current goal using mul_SNo_com (1 + (v + - x) * w') (recip_SNo_pos v) (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) Hrv1 (from left to right).
We will prove 1 ≤ 1 + v * y + - v * recip_SNo_pos v * (1 + (v + - x) * w').
rewrite the current goal using mul_SNo_assoc v (recip_SNo_pos v) (1 + (v + - x) * w') Hv1 Hrv1 (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (from left to right).
We will prove 1 ≤ 1 + v * y + - (v * recip_SNo_pos v) * (1 + (v + - x) * w').
rewrite the current goal using Hrv2 (from left to right).
We will prove 1 ≤ 1 + v * y + - 1 * (1 + (v + - x) * w').
rewrite the current goal using mul_SNo_oneL (1 + (v + - x) * w') (SNo_add_SNo 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (from left to right).
We will prove 1 ≤ 1 + v * y + - (1 + (v + - x) * w').
rewrite the current goal using minus_add_SNo_distr 1 ((v + - x) * w') SNo_1 (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw') (from left to right).
We will prove 1 ≤ 1 + v * y + - 1 + - (v + - x) * w'.
rewrite the current goal using add_SNo_rotate_3_1 (- 1) (- (v + - x) * w') (v * y) (SNo_minus_SNo 1 SNo_1) (SNo_minus_SNo ((v + - x) * w') (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (SNo_mul_SNo v y Hv1 H1) (from right to left).
We will prove 1 ≤ 1 + - 1 + - (v + - x) * w' + v * y.
rewrite the current goal using add_SNo_minus_SNo_prop2 1 (- (v + - x) * w' + v * y) SNo_1 (SNo_add_SNo (- (v + - x) * w') (v * y) (SNo_minus_SNo ((v + - x) * w') (SNo_mul_SNo (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw')) (SNo_mul_SNo v y Hv1 H1)) (from left to right).
We will prove 1 ≤ - (v + - x) * w' + v * y.
rewrite the current goal using mul_SNo_minus_distrL (v + - x) w' (SNo_add_SNo v (- x) Hv1 (SNo_minus_SNo x Hx)) Hw' (from right to left).
We will prove 1 ≤ (- (v + - x)) * w' + v * y.
rewrite the current goal using minus_add_SNo_distr v (- x) Hv1 (SNo_minus_SNo x Hx) (from left to right).
rewrite the current goal using minus_SNo_invol x Hx (from left to right).
We will prove 1 ≤ (- v + x) * w' + v * y.
Apply SNoLe_tra 1 ((- v + x) * w + v * y) ((- v + x) * w' + v * y) SNo_1 (SNo_add_SNo ((- v + x) * w) (v * y) (SNo_mul_SNo (- v + x) w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw1) (SNo_mul_SNo v y Hv1 H1)) (SNo_add_SNo ((- v + x) * w') (v * y) (SNo_mul_SNo (- v + x) w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw') (SNo_mul_SNo v y Hv1 H1)) to the current goal.
We will prove 1 ≤ (- v + x) * w + v * y.
rewrite the current goal using mul_SNo_distrR (- v) x w (SNo_minus_SNo v Hv1) Hx Hw1 (from left to right).
We will prove 1 ≤ ((- v) * w + x * w) + v * y.
rewrite the current goal using mul_SNo_minus_distrL v w Hv1 Hw1 (from left to right).
We will prove 1 ≤ (- v * w + x * w) + v * y.
rewrite the current goal using add_SNo_assoc (- v * w) (x * w) (v * y) (SNo_minus_SNo (v * w) (SNo_mul_SNo v w Hv1 Hw1)) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1) (from right to left).
We will prove 1 ≤ - v * w + x * w + v * y.
rewrite the current goal using add_SNo_com (- v * w) (x * w + v * y) (SNo_minus_SNo (v * w) (SNo_mul_SNo v w Hv1 Hw1)) (SNo_add_SNo (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1)) (from left to right).
We will prove 1 ≤ (x * w + v * y) + - v * w.
Apply add_SNo_minus_Le2b (x * w + v * y) (v * w) 1 (SNo_add_SNo (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1)) (SNo_mul_SNo v w Hv1 Hw1) SNo_1 to the current goal.
We will prove 1 + v * w ≤ x * w + v * y.
rewrite the current goal using add_SNo_com (x * w) (v * y) (SNo_mul_SNo x w Hx Hw1) (SNo_mul_SNo v y Hv1 H1) (from left to right).
We will prove 1 + v * w ≤ v * y + x * w.
An exact proof term for the current goal is H7.
We will prove (- v + x) * w + v * y ≤ (- v + x) * w' + v * y.
Apply add_SNo_Le1 ((- v + x) * w) (v * y) ((- v + x) * w') (SNo_mul_SNo (- v + x) w (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw1) (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo (- v + x) w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) Hw') to the current goal.
We will prove (- v + x) * w ≤ (- v + x) * w'.
An exact proof term for the current goal is H8.
We will prove 1 + v * (y + - w'') < 1.
rewrite the current goal using add_SNo_0R 1 SNo_1 (from right to left) at position 4.
We will prove 1 + v * (y + - w'') < 1 + 0.
Apply add_SNo_Lt2 1 (v * (y + - w'')) 0 SNo_1 (SNo_mul_SNo v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1))) SNo_0 to the current goal.
We will prove v * (y + - w'') < 0.
Apply mul_SNo_pos_neg v (y + - w'') Hv1 (SNo_add_SNo y (- w'') H1 (SNo_minus_SNo w'' Lw''1)) Hvpos to the current goal.
We will prove y + - w'' < 0.
Apply add_SNo_minus_Lt1b y w'' 0 H1 Lw''1 SNo_0 to the current goal.
We will prove y < 0 + w''.
rewrite the current goal using add_SNo_0L w'' Lw''1 (from left to right).
We will prove y < w''.
An exact proof term for the current goal is H4 w'' Hw''.
Apply mul_SNo_SNoL_interpolate_impred x y Hx H1 1 L10 to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Let w be given.
Assume Hw: w ∈ SNoL y.
Assume H7: 1 + v * w ≤ v * y + x * w.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
Apply SNoL_E y H1 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: w < y.
We prove the intermediate claim LvS: v ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 v x Hv1 Hx Hv2.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
Apply L6 w Hw to the current goal.
Let w' be given.
Assume Hw'.
Apply Hw' to the current goal.
Assume Hw'1: w' ∈ L.
Assume Hw'2: w ≤ w'.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HL w' Hw'1.
We prove the intermediate claim Lxw': SNo (x * w').
An exact proof term for the current goal is SNo_mul_SNo x w' Hx Lw'.
We prove the intermediate claim Lvpos: 0 < v.
Apply SNoLtLe_or 0 v SNo_0 Hv1 to the current goal.
Assume H8: 0 < v.
An exact proof term for the current goal is H8.
Assume H8: v ≤ 0.
We will prove False.
Apply SNoLt_irref 1 to the current goal.
We will prove 1 < 1.
Apply SNoLeLt_tra 1 (x * w') 1 SNo_1 Lxw' SNo_1 to the current goal.
We will prove 1 ≤ x * w'.
Apply SNoLe_tra 1 (x * w) (x * w') SNo_1 Lxw Lxw' to the current goal.
We will prove 1 ≤ x * w.
Apply SNoLe_tra 1 (v * (y + - w) + x * w) (x * w) SNo_1 (SNo_add_SNo (v * (y + - w)) (x * w) (SNo_mul_SNo v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1))) Lxw) Lxw to the current goal.
We will prove 1 ≤ v * (y + - w) + x * w.
rewrite the current goal using mul_SNo_distrL v y (- w) Hv1 H1 (SNo_minus_SNo w Hw1) (from left to right).
We will prove 1 ≤ (v * y + v * (- w)) + x * w.
rewrite the current goal using add_SNo_com_3b_1_2 (v * y) (v * (- w)) (x * w) (SNo_mul_SNo v y Hv1 H1) (SNo_mul_SNo v (- w) Hv1 (SNo_minus_SNo w Hw1)) Lxw (from left to right).
We will prove 1 ≤ (v * y + x * w) + v * (- w).
rewrite the current goal using mul_SNo_minus_distrR v w Hv1 Hw1 (from left to right).
We will prove 1 ≤ (v * y + x * w) + - v * w.
Apply add_SNo_minus_Le2b (v * y + x * w) (v * w) 1 (SNo_add_SNo (v * y) (x * w) (SNo_mul_SNo v y Hv1 H1) Lxw) (SNo_mul_SNo v w Hv1 Hw1) SNo_1 to the current goal.
We will prove 1 + v * w ≤ v * y + x * w.
An exact proof term for the current goal is H7.
We will prove v * (y + - w) + x * w ≤ x * w.
rewrite the current goal using add_SNo_0L (x * w) Lxw (from right to left) at position 2.
We will prove v * (y + - w) + x * w ≤ 0 + x * w.
Apply add_SNo_Le1 (v * (y + - w)) (x * w) 0 (SNo_mul_SNo v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1))) Lxw SNo_0 to the current goal.
We will prove v * (y + - w) ≤ 0.
Apply mul_SNo_nonpos_pos v (y + - w) Hv1 (SNo_add_SNo y (- w) H1 (SNo_minus_SNo w Hw1)) H8 to the current goal.
We will prove 0 < y + - w.
Apply add_SNo_minus_Lt2b y w 0 H1 Hw1 SNo_0 to the current goal.
We will prove 0 + w < y.
rewrite the current goal using add_SNo_0L w Hw1 (from left to right).
We will prove w < y.
An exact proof term for the current goal is Hw3.
We will prove x * w ≤ x * w'.
An exact proof term for the current goal is nonneg_mul_SNo_Le x w w' Hx (SNoLtLe 0 x Hxpos) Hw1 Lw' Hw'2.
We will prove x * w' < 1.
An exact proof term for the current goal is L1L w' Hw'1.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw'': w'' ∈ R.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 0) w' Hw'1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H9: w' ∈ SNo_recipaux x recip_SNo_pos k 0.
Apply famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) (ordsucc k) w'' (omega_ordsucc k Hk) to the current goal.
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos (ordsucc k) 1.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos k 1 ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos.
Apply binunionI1 to the current goal.
Apply binunionI2 to the current goal.
We will prove w'' ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos.
Apply SNo_recipauxset_I (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos to the current goal.
We will prove w' ∈ SNo_recipaux x recip_SNo_pos k 0.
An exact proof term for the current goal is H9.
We will prove v ∈ SNoL_pos x.
We will prove v ∈ {w ∈ SNoL x|0 < w}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hv.
We will prove 0 < v.
An exact proof term for the current goal is Lvpos.
Apply L11 v w w' Hv1 Hw1 Lw' LvS Lvpos H7 Lw'' to the current goal.
We will prove (- v + x) * w ≤ (- v + x) * w'.
Apply nonneg_mul_SNo_Le (- v + x) w w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) to the current goal.
We will prove 0 ≤ - v + x.
rewrite the current goal using add_SNo_com (- v) x (SNo_minus_SNo v Hv1) Hx (from left to right).
We will prove 0 ≤ x + - v.
Apply add_SNo_minus_Le2b x v 0 Hx Hv1 SNo_0 to the current goal.
We will prove 0 + v ≤ x.
rewrite the current goal using add_SNo_0L v Hv1 (from left to right).
We will prove v ≤ x.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hv3.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Lw'.
An exact proof term for the current goal is Hw'2.
Let v be given.
Assume Hv: v ∈ SNoR x.
Let w be given.
Assume Hw: w ∈ SNoR y.
Assume H7: 1 + v * w ≤ v * y + x * w.
Apply SNoR_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: x < v.
Apply SNoR_E y H1 w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: y < w.
We prove the intermediate claim LvS: v ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 v x Hv1 Hx Hv2.
We prove the intermediate claim Lvpos: 0 < v.
An exact proof term for the current goal is SNoLt_tra 0 x v SNo_0 Hx Hv1 Hxpos Hv3.
We prove the intermediate claim Lxw: SNo (x * w).
An exact proof term for the current goal is SNo_mul_SNo x w Hx Hw1.
Apply L7 w Hw to the current goal.
Let w' be given.
Assume Hw'.
Apply Hw' to the current goal.
Assume Hw'1: w' ∈ R.
Assume Hw'2: w' ≤ w.
We prove the intermediate claim Lw': SNo w'.
An exact proof term for the current goal is HR w' Hw'1.
We prove the intermediate claim Lxw': SNo (x * w').
An exact proof term for the current goal is SNo_mul_SNo x w' Hx Lw'.
Set w'' to be the term (1 + (v + - x) * w') * recip_SNo_pos v.
We prove the intermediate claim Lw'': w'' ∈ R.
Apply famunionE_impred ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) w' Hw'1 to the current goal.
Let k be given.
Assume Hk: k ∈ ω.
Assume H9: w' ∈ SNo_recipaux x recip_SNo_pos k 1.
Apply famunionI ω (λk ⇒ SNo_recipaux x recip_SNo_pos k 1) (ordsucc k) w'' (omega_ordsucc k Hk) to the current goal.
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos (ordsucc k) 1.
rewrite the current goal using SNo_recipaux_S x recip_SNo_pos k (omega_nat_p k Hk) (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove w'' ∈ SNo_recipaux x recip_SNo_pos k 1 ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 0) x (SNoL_pos x) recip_SNo_pos ∪ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos.
Apply binunionI2 to the current goal.
We will prove w'' ∈ SNo_recipauxset (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos.
Apply SNo_recipauxset_I (SNo_recipaux x recip_SNo_pos k 1) x (SNoR x) recip_SNo_pos to the current goal.
We will prove w' ∈ SNo_recipaux x recip_SNo_pos k 1.
An exact proof term for the current goal is H9.
We will prove v ∈ SNoR x.
An exact proof term for the current goal is Hv.
Apply L11 v w w' Hv1 Hw1 Lw' LvS Lvpos H7 Lw'' to the current goal.
We will prove (- v + x) * w ≤ (- v + x) * w'.
Apply L11 v w w' Hv1 Hw1 Lw' LvS Lvpos H7 Lw'' to the current goal.
We will prove (- v + x) * w ≤ (- v + x) * w'.
Apply nonpos_mul_SNo_Le (- v + x) w w' (SNo_add_SNo (- v) x (SNo_minus_SNo v Hv1) Hx) to the current goal.
We will prove - v + x ≤ 0.
rewrite the current goal using add_SNo_com (- v) x (SNo_minus_SNo v Hv1) Hx (from left to right).
We will prove x + - v ≤ 0.
Apply add_SNo_minus_Le2 0 (- v) x SNo_0 (SNo_minus_SNo v Hv1) Hx to the current goal.
rewrite the current goal using minus_SNo_invol v Hv1 (from left to right).
We will prove x ≤ 0 + v.
rewrite the current goal using add_SNo_0L v Hv1 (from left to right).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hv3.
An exact proof term for the current goal is Hw1.
An exact proof term for the current goal is Lw'.
An exact proof term for the current goal is Hw'2.
∎