Let a, b, c and y be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Assume HyR: y ∈ R.
Assume Hb0: b = 0.
Assume Ha0: a ≠ 0.
We will prove apply_fun (affine_line_R2_param_by_y a b c) y ∈ affine_line_R2 a b c.
rewrite the current goal using (affine_line_R2_param_by_y_apply a b c y HyR) (from left to right).
Set x0 to be the term div_SNo c a.
We will prove (x0,y) ∈ affine_line_R2 a b c.
We prove the intermediate claim Hdef: affine_line_R2 a b c = {p ∈ EuclidPlane|add_SNo (mul_SNo a (R2_xcoord p)) (mul_SNo b (R2_ycoord p)) = c}.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
We prove the intermediate claim HxyPlane: (x0,y) ∈ EuclidPlane.
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 HxReal: x0 ∈ real.
An exact proof term for the current goal is (real_div_SNo c HcReal a HaReal).
We prove the intermediate claim HxR: x0 ∈ R.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is HxReal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x0 y HxR HyR).
We prove the intermediate claim Hprop: add_SNo (mul_SNo a (R2_xcoord (x0,y))) (mul_SNo b (R2_ycoord (x0,y))) = c.
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 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 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 (R2_xcoord_tuple x0 y) (from left to right).
rewrite the current goal using (R2_ycoord_tuple x0 y) (from left to right).
rewrite the current goal using Hb0 (from left to right).
We prove the intermediate claim HyReal: y ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HyR.
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (real_SNo y HyReal).
rewrite the current goal using (mul_SNo_zeroL y HyS) (from left to right).
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.
An exact proof term for the current goal is (SepI EuclidPlane (λp0 : set ⇒ add_SNo (mul_SNo a (R2_xcoord p0)) (mul_SNo b (R2_ycoord p0)) = c) (x0,y) HxyPlane Hprop).
∎