Let a, b, c, x1 and x2 be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Assume Hbne: b ≠ 0.
Assume Hsign: same_sign_nonzero_R a b.
Assume Hx1R: x1 ∈ R.
Assume Hx2R: x2 ∈ R.
Assume Hx12: Rlt x1 x2.
We will prove Rlt (div_SNo (add_SNo c (minus_SNo (mul_SNo a x2))) b) (div_SNo (add_SNo c (minus_SNo (mul_SNo a x1))) b).
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim HaReal: a ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HaR.
We prove the intermediate claim HbReal: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim HcReal: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
We prove the intermediate claim Hx1Real: x1 ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hx1R.
We prove the intermediate claim Hx2Real: x2 ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hx2R.
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaReal).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbReal).
We prove the intermediate claim HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcReal).
We prove the intermediate claim Hx1S: SNo x1.
An exact proof term for the current goal is (real_SNo x1 Hx1Real).
We prove the intermediate claim Hx2S: SNo x2.
An exact proof term for the current goal is (real_SNo x2 Hx2Real).
We prove the intermediate claim Hx12lt: x1 < x2.
An exact proof term for the current goal is (RltE_lt x1 x2 Hx12).
Set num1 to be the term add_SNo c (minus_SNo (mul_SNo a x1)).
Set num2 to be the term add_SNo c (minus_SNo (mul_SNo a x2)).
We prove the intermediate claim Hnum1S: SNo num1.
An exact proof term for the current goal is (SNo_add_SNo c (minus_SNo (mul_SNo a x1)) HcS (SNo_minus_SNo (mul_SNo a x1) (SNo_mul_SNo a x1 HaS Hx1S))).
We prove the intermediate claim Hnum2S: SNo num2.
An exact proof term for the current goal is (SNo_add_SNo c (minus_SNo (mul_SNo a x2)) HcS (SNo_minus_SNo (mul_SNo a x2) (SNo_mul_SNo a x2 HaS Hx2S))).
We prove the intermediate claim Hy1Real: div_SNo (add_SNo c (minus_SNo (mul_SNo a x1))) b ∈ real.
An exact proof term for the current goal is (real_div_SNo (add_SNo c (minus_SNo (mul_SNo a x1))) (real_add_SNo c HcReal (minus_SNo (mul_SNo a x1)) (real_minus_SNo (mul_SNo a x1) (real_mul_SNo a HaReal x1 Hx1Real))) b HbReal).
We prove the intermediate claim Hy2Real: div_SNo (add_SNo c (minus_SNo (mul_SNo a x2))) b ∈ real.
An exact proof term for the current goal is (real_div_SNo (add_SNo c (minus_SNo (mul_SNo a x2))) (real_add_SNo c HcReal (minus_SNo (mul_SNo a x2)) (real_minus_SNo (mul_SNo a x2) (real_mul_SNo a HaReal x2 Hx2Real))) b HbReal).
We prove the intermediate claim Hy1R: div_SNo (add_SNo c (minus_SNo (mul_SNo a x1))) b ∈ R.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hy1Real.
We prove the intermediate claim Hy2R: div_SNo (add_SNo c (minus_SNo (mul_SNo a x2))) b ∈ R.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hy2Real.
Apply Hsign to the current goal.
Assume Hpos: Rlt 0 a ∧ Rlt 0 b.
We prove the intermediate claim H0a: Rlt 0 a.
An exact proof term for the current goal is (andEL (Rlt 0 a) (Rlt 0 b) Hpos).
We prove the intermediate claim H0b: Rlt 0 b.
An exact proof term for the current goal is (andER (Rlt 0 a) (Rlt 0 b) Hpos).
We prove the intermediate claim H0alt: 0 < a.
An exact proof term for the current goal is (RltE_lt 0 a H0a).
We prove the intermediate claim H0blt: 0 < b.
An exact proof term for the current goal is (RltE_lt 0 b H0b).
We prove the intermediate claim Hax1ax2: mul_SNo a x1 < mul_SNo a x2.
An exact proof term for the current goal is (pos_mul_SNo_Lt a x1 x2 HaS H0alt Hx1S Hx2S Hx12lt).
We prove the intermediate claim HmAx2mAx1: minus_SNo (mul_SNo a x2) < minus_SNo (mul_SNo a x1).
An exact proof term for the current goal is (minus_SNo_Lt_contra (mul_SNo a x1) (mul_SNo a x2) (SNo_mul_SNo a x1 HaS Hx1S) (SNo_mul_SNo a x2 HaS Hx2S) Hax1ax2).
We prove the intermediate claim Hnum2num1: num2 < num1.
An exact proof term for the current goal is (add_SNo_Lt2 c (minus_SNo (mul_SNo a x2)) (minus_SNo (mul_SNo a x1)) HcS (SNo_minus_SNo (mul_SNo a x2) (SNo_mul_SNo a x2 HaS Hx2S)) (SNo_minus_SNo (mul_SNo a x1) (SNo_mul_SNo a x1 HaS Hx1S)) HmAx2mAx1).
We prove the intermediate claim HrecipPos: 0 < recip_SNo b.
An exact proof term for the current goal is (recip_SNo_of_pos_is_pos b HbS H0blt).
We prove the intermediate claim HrecipS: SNo (recip_SNo b).
An exact proof term for the current goal is (SNo_recip_SNo b HbS).
We prove the intermediate claim HdivLt: div_SNo num2 b < div_SNo num1 b.
We prove the intermediate claim Heq2: div_SNo num2 b = mul_SNo num2 (recip_SNo b).
Use reflexivity.
We prove the intermediate claim Heq1: div_SNo num1 b = mul_SNo num1 (recip_SNo b).
Use reflexivity.
rewrite the current goal using Heq2 (from left to right).
rewrite the current goal using Heq1 (from left to right).
An exact proof term for the current goal is (pos_mul_SNo_Lt' num2 num1 (recip_SNo b) Hnum2S Hnum1S HrecipS HrecipPos Hnum2num1).
An exact proof term for the current goal is (RltI (div_SNo num2 b) (div_SNo num1 b) Hy2R Hy1R HdivLt).
Assume Hneg: Rlt a 0 ∧ Rlt b 0.
We prove the intermediate claim Ha0: Rlt a 0.
An exact proof term for the current goal is (andEL (Rlt a 0) (Rlt b 0) Hneg).
We prove the intermediate claim Hb0: Rlt b 0.
An exact proof term for the current goal is (andER (Rlt a 0) (Rlt b 0) Hneg).
We prove the intermediate claim Halt0: a < 0.
An exact proof term for the current goal is (RltE_lt a 0 Ha0).
We prove the intermediate claim Hblt0: b < 0.
An exact proof term for the current goal is (RltE_lt b 0 Hb0).
We prove the intermediate claim Hax2ax1: mul_SNo a x2 < mul_SNo a x1.
An exact proof term for the current goal is (neg_mul_SNo_Lt a x2 x1 HaS Halt0 Hx2S Hx1S Hx12lt).
We prove the intermediate claim HmAx1mAx2: minus_SNo (mul_SNo a x1) < minus_SNo (mul_SNo a x2).
An exact proof term for the current goal is (minus_SNo_Lt_contra (mul_SNo a x2) (mul_SNo a x1) (SNo_mul_SNo a x2 HaS Hx2S) (SNo_mul_SNo a x1 HaS Hx1S) Hax2ax1).
We prove the intermediate claim Hnum1num2: num1 < num2.
An exact proof term for the current goal is (add_SNo_Lt2 c (minus_SNo (mul_SNo a x1)) (minus_SNo (mul_SNo a x2)) HcS (SNo_minus_SNo (mul_SNo a x1) (SNo_mul_SNo a x1 HaS Hx1S)) (SNo_minus_SNo (mul_SNo a x2) (SNo_mul_SNo a x2 HaS Hx2S)) HmAx1mAx2).
We prove the intermediate claim HrecipNeg: recip_SNo b < 0.
We prove the intermediate claim HminusbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim HminusbPos: 0 < minus_SNo b.
We prove the intermediate claim H0ltminusb: minus_SNo 0 < minus_SNo b.
An exact proof term for the current goal is (minus_SNo_Lt_contra b 0 HbS SNo_0 Hblt0).
We will prove 0 < minus_SNo b.
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is H0ltminusb.
We prove the intermediate claim HrecipPosDef: recip_SNo b = minus_SNo (recip_SNo_pos (minus_SNo b)).
rewrite the current goal using (recip_SNo_negcase b HbS Hblt0) (from left to right).
Use reflexivity.
We prove the intermediate claim HtS: SNo (recip_SNo_pos (minus_SNo b)).
An exact proof term for the current goal is (SNo_recip_SNo_pos (minus_SNo b) HminusbS HminusbPos).
We prove the intermediate claim HtPos: 0 < recip_SNo_pos (minus_SNo b).
An exact proof term for the current goal is (recip_SNo_pos_is_pos (minus_SNo b) HminusbS HminusbPos).
rewrite the current goal using HrecipPosDef (from left to right).
We prove the intermediate claim HnegT: minus_SNo (recip_SNo_pos (minus_SNo b)) < 0.
We prove the intermediate claim Hmtltm0: minus_SNo (recip_SNo_pos (minus_SNo b)) < minus_SNo 0.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 (recip_SNo_pos (minus_SNo b)) SNo_0 HtS HtPos).
We will prove minus_SNo (recip_SNo_pos (minus_SNo b)) < 0.
rewrite the current goal using (minus_SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is Hmtltm0.
An exact proof term for the current goal is HnegT.
We prove the intermediate claim HrecipS: SNo (recip_SNo b).
An exact proof term for the current goal is (SNo_recip_SNo b HbS).
We prove the intermediate claim HdivLt: div_SNo num2 b < div_SNo num1 b.
We prove the intermediate claim Heq2: div_SNo num2 b = mul_SNo num2 (recip_SNo b).
Use reflexivity.
We prove the intermediate claim Heq1: div_SNo num1 b = mul_SNo num1 (recip_SNo b).
Use reflexivity.
rewrite the current goal using Heq2 (from left to right).
rewrite the current goal using Heq1 (from left to right).
rewrite the current goal using (mul_SNo_com num2 (recip_SNo b) Hnum2S HrecipS) (from left to right).
rewrite the current goal using (mul_SNo_com num1 (recip_SNo b) Hnum1S HrecipS) (from left to right).
An exact proof term for the current goal is (neg_mul_SNo_Lt (recip_SNo b) num2 num1 HrecipS HrecipNeg Hnum2S Hnum1S Hnum1num2).
An exact proof term for the current goal is (RltI (div_SNo num2 b) (div_SNo num1 b) Hy2R Hy1R HdivLt).
∎