Let a, b and c be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Assume Hb0: b = 0.
Assume Ha0: a ≠ 0.
Set x0 to be the term div_SNo c a.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ affine_line_R2 a b c.
We will prove p ∈ setprod {x0} R.
We prove the intermediate claim HpRR: p ∈ setprod R R.
An exact proof term for the current goal is (affine_line_R2_subset_R2 a b c p Hp).
We prove the intermediate claim Hp0R: (p 0) ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p HpRR).
We prove the intermediate claim Hp1R: (p 1) ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) p HpRR).
We prove the intermediate claim Heqdef: add_SNo (mul_SNo a (R2_xcoord p)) (mul_SNo b (R2_ycoord p)) = c.
An exact proof term for the current goal is (SepE2 EuclidPlane (λp0 : set ⇒ add_SNo (mul_SNo a (R2_xcoord p0)) (mul_SNo b (R2_ycoord p0)) = c) p Hp).
We prove the intermediate claim Hxdef: R2_xcoord p = p 0.
Use reflexivity.
We prove the intermediate claim Hydef: R2_ycoord p = p 1.
Use reflexivity.
We prove the intermediate claim Hmul: mul_SNo a (p 0) = c.
We prove the intermediate claim Heq0: add_SNo (mul_SNo a (p 0)) (mul_SNo b (p 1)) = c.
rewrite the current goal using Hxdef (from right to left).
rewrite the current goal using Hydef (from right to left).
An exact proof term for the current goal is Heqdef.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim Hp1Real: (p 1) ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hp1R.
We prove the intermediate claim Hp1S: SNo (p 1).
An exact proof term for the current goal is (real_SNo (p 1) Hp1Real).
We prove the intermediate claim Hbterm: mul_SNo b (p 1) = 0.
rewrite the current goal using Hb0 (from left to right).
An exact proof term for the current goal is (mul_SNo_zeroL (p 1) Hp1S).
We prove the intermediate claim Heq2: add_SNo (mul_SNo a (p 0)) 0 = c.
We prove the intermediate claim HlhsEq: add_SNo (mul_SNo a (p 0)) (mul_SNo b (p 1)) = add_SNo (mul_SNo a (p 0)) 0.
rewrite the current goal using Hbterm (from left to right).
Use reflexivity.
rewrite the current goal using HlhsEq (from right to left).
An exact proof term for the current goal is Heq0.
We prove the intermediate claim Hap0: SNo (mul_SNo a (p 0)).
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 Hp0Real: (p 0) ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hp0R.
An exact proof term for the current goal is (SNo_mul_SNo a (p 0) (real_SNo a HaReal) (real_SNo (p 0) Hp0Real)).
rewrite the current goal using (add_SNo_0R (mul_SNo a (p 0)) Hap0) (from right to left).
An exact proof term for the current goal is Heq2.
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 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 Hp0Real: (p 0) ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hp0R.
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcReal).
We prove the intermediate claim Hp0S: SNo (p 0).
An exact proof term for the current goal is (real_SNo (p 0) Hp0Real).
We prove the intermediate claim Hmul2: c = mul_SNo a (p 0).
rewrite the current goal using Hmul (from left to right).
Use reflexivity.
We prove the intermediate claim HdivEq: div_SNo c a = (p 0).
An exact proof term for the current goal is (mul_div_SNo_nonzero_eq c a (p 0) HcS HaS Hp0S Ha0 Hmul2).
We prove the intermediate claim Hx0def: x0 = div_SNo c a.
Use reflexivity.
We prove the intermediate claim Hx0eq: x0 = (p 0).
rewrite the current goal using Hx0def (from left to right).
An exact proof term for the current goal is HdivEq.
We prove the intermediate claim Hp0Sing: (p 0) ∈ {x0}.
rewrite the current goal using Hx0eq (from right to left).
An exact proof term for the current goal is (SingI x0).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta R R p HpRR).
rewrite the current goal using Heta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x0} R (p 0) (p 1) Hp0Sing Hp1R).
Let p be given.
Assume Hp: p ∈ setprod {x0} R.
We will prove p ∈ affine_line_R2 a b c.
We prove the intermediate claim Hp0Sing: (p 0) ∈ {x0}.
An exact proof term for the current goal is (ap0_Sigma {x0} (λ_ : set ⇒ R) p Hp).
We prove the intermediate claim Hp1R: (p 1) ∈ R.
An exact proof term for the current goal is (ap1_Sigma {x0} (λ_ : set ⇒ R) p Hp).
We prove the intermediate claim Hp0eq: (p 0) = x0.
An exact proof term for the current goal is (singleton_elem (p 0) x0 Hp0Sing).
We prove the intermediate claim HpRR: p ∈ setprod R R.
We prove the intermediate claim HSingSub: {x0} ⊆ R.
We prove the intermediate claim Hx0Real: x0 ∈ real.
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 HcReal: c ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HcR.
An exact proof term for the current goal is (real_div_SNo c HcReal a HaReal).
We prove the intermediate claim Hx0R: x0 ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hx0Real.
An exact proof term for the current goal is (singleton_subset x0 R Hx0R).
An exact proof term for the current goal is (setprod_Subq {x0} R R R HSingSub (Subq_ref R) p Hp).
We prove the intermediate claim Hdef: affine_line_R2 a b c = {q ∈ EuclidPlane|add_SNo (mul_SNo a (R2_xcoord q)) (mul_SNo b (R2_ycoord q)) = c}.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
We prove the intermediate claim HxyPlane: p ∈ EuclidPlane.
We prove the intermediate claim Heq: EuclidPlane = setprod R R.
Use reflexivity.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HpRR.
We will prove p ∈ {q ∈ EuclidPlane|add_SNo (mul_SNo a (R2_xcoord q)) (mul_SNo b (R2_ycoord q)) = c}.
Apply (SepI EuclidPlane (λq : set ⇒ add_SNo (mul_SNo a (R2_xcoord q)) (mul_SNo b (R2_ycoord q)) = c) p HxyPlane) to the current goal.
We prove the intermediate claim Hxdef: R2_xcoord p = p 0.
Use reflexivity.
We prove the intermediate claim Hydef: R2_ycoord p = p 1.
Use reflexivity.
rewrite the current goal using Hxdef (from left to right).
rewrite the current goal using Hydef (from left to right).
rewrite the current goal using Hb0 (from left to right).
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 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 Hp1Real: (p 1) ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hp1R.
We prove the intermediate claim Hp1S: SNo (p 1).
An exact proof term for the current goal is (real_SNo (p 1) Hp1Real).
rewrite the current goal using (mul_SNo_zeroL (p 1) Hp1S) (from left to right).
rewrite the current goal using Hp0eq (from left to right).
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 HcS: SNo c.
An exact proof term for the current goal is (real_SNo c HcReal).
We prove the intermediate claim Hx0Real: x0 ∈ real.
An exact proof term for the current goal is (real_div_SNo c HcReal a HaReal).
We prove the intermediate claim Hx0S: SNo x0.
An exact proof term for the current goal is (real_SNo x0 Hx0Real).
rewrite the current goal using (add_SNo_0R (mul_SNo a x0) (SNo_mul_SNo a x0 HaS Hx0S)) (from left to right).
We prove the intermediate claim Hmul: mul_SNo a x0 = c.
We prove the intermediate claim Hx0def: x0 = div_SNo c a.
Use reflexivity.
rewrite the current goal using Hx0def (from left to right).
rewrite the current goal using (mul_div_SNo_invR c a HcS HaS Ha0) (from left to right).
Use reflexivity.
An exact proof term for the current goal is Hmul.
∎