Let a, b, c and p be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Assume Hbne: b ≠ 0.
Assume Hp: p ∈ affine_line_R2 a b c.
We will prove apply_fun (affine_line_R2_param_by_x a b c) (apply_fun (projection1 R R) p) = p.
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 Hpeta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta R R p HpRR).
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 Happ1: apply_fun (projection1 R R) p = p 0.
An exact proof term for the current goal is (projection1_apply R R p HpRR).
rewrite the current goal using Happ1 (from left to right).
rewrite the current goal using (affine_line_R2_param_by_x_apply a b c (p 0) Hp0R) (from left to right).
rewrite the current goal using Hpeta (from left to right) at position 3.
We prove the intermediate claim Hycoord: div_SNo (add_SNo c (minus_SNo (mul_SNo a (p 0)))) b = p 1.
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 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 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 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 Hp0S: SNo (p 0).
An exact proof term for the current goal is (real_SNo (p 0) Hp0Real).
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 HaxS: SNo (mul_SNo a (p 0)).
An exact proof term for the current goal is (SNo_mul_SNo a (p 0) HaS Hp0S).
We prove the intermediate claim HbyS: SNo (mul_SNo b (p 1)).
An exact proof term for the current goal is (SNo_mul_SNo b (p 1) HbS Hp1S).
We prove the intermediate claim HmAxS: SNo (minus_SNo (mul_SNo a (p 0))).
An exact proof term for the current goal is (SNo_minus_SNo (mul_SNo a (p 0)) HaxS).
We prove the intermediate claim Hline0: 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 Hline: add_SNo (mul_SNo a (p 0)) (mul_SNo b (p 1)) = c.
We prove the intermediate claim Hxcoord: R2_xcoord p = p 0.
Use reflexivity.
We prove the intermediate claim Hycoord0: R2_ycoord p = p 1.
Use reflexivity.
rewrite the current goal using Hxcoord (from right to left).
rewrite the current goal using Hycoord0 (from right to left).
An exact proof term for the current goal is Hline0.
We prove the intermediate claim HbyEq: add_SNo c (minus_SNo (mul_SNo a (p 0))) = mul_SNo b (p 1).
rewrite the current goal using Hline (from right to left) at position 1.
rewrite the current goal using (add_SNo_assoc (mul_SNo a (p 0)) (mul_SNo b (p 1)) (minus_SNo (mul_SNo a (p 0))) HaxS HbyS HmAxS) (from right to left).
rewrite the current goal using (add_SNo_com (mul_SNo b (p 1)) (minus_SNo (mul_SNo a (p 0))) HbyS HmAxS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_assoc (mul_SNo a (p 0)) (minus_SNo (mul_SNo a (p 0))) (mul_SNo b (p 1)) HaxS HmAxS HbyS) (from left to right).
rewrite the current goal using (add_SNo_minus_SNo_rinv (mul_SNo a (p 0)) HaxS) (from left to right).
An exact proof term for the current goal is (add_SNo_0L (mul_SNo b (p 1)) HbyS).
We prove the intermediate claim HxtermS: SNo (add_SNo c (minus_SNo (mul_SNo a (p 0)))).
An exact proof term for the current goal is (SNo_add_SNo c (minus_SNo (mul_SNo a (p 0))) HcS HmAxS).
An exact proof term for the current goal is (mul_div_SNo_nonzero_eq (add_SNo c (minus_SNo (mul_SNo a (p 0)))) b (p 1) HxtermS HbS Hp1S Hbne HbyEq).
rewrite the current goal using Hycoord (from left to right).
Use reflexivity.
∎