Let a, b, c and x be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Assume HxR: x ∈ R.
Assume Hb0: b ≠ 0.
We will prove apply_fun (affine_line_R2_param_by_x a b c) x ∈ affine_line_R2 a b c.
rewrite the current goal using (affine_line_R2_param_by_x_apply a b c x HxR) (from left to right).
Set y to be the term div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b.
We prove the intermediate claim Hydef: y = div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b.
Use reflexivity.
rewrite the current goal using Hydef (from right to left).
We will prove (x,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: (x,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 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 HxReal: x ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
We prove the intermediate claim HmulReal: mul_SNo a x ∈ real.
An exact proof term for the current goal is (real_mul_SNo a HaReal x HxReal).
We prove the intermediate claim HmReal: minus_SNo (mul_SNo a x) ∈ real.
An exact proof term for the current goal is (real_minus_SNo (mul_SNo a x) HmulReal).
We prove the intermediate claim HnumReal: add_SNo c (minus_SNo (mul_SNo a x)) ∈ real.
An exact proof term for the current goal is (real_add_SNo c HcReal (minus_SNo (mul_SNo a x)) HmReal).
We prove the intermediate claim HyReal: y ∈ real.
rewrite the current goal using Hydef (from left to right).
An exact proof term for the current goal is (real_div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) HnumReal b HbReal).
We prove the intermediate claim HyR: y ∈ R.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is HyReal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x y HxR HyR).
We prove the intermediate claim Hprop: add_SNo (mul_SNo a (R2_xcoord (x,y))) (mul_SNo b (R2_ycoord (x,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 HxReal: x ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
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 HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxReal).
We prove the intermediate claim HaxS: SNo (mul_SNo a x).
An exact proof term for the current goal is (SNo_mul_SNo a x HaS HxS).
We prove the intermediate claim HnumS: SNo (add_SNo c (minus_SNo (mul_SNo a x))).
An exact proof term for the current goal is (SNo_add_SNo c (minus_SNo (mul_SNo a x)) HcS (SNo_minus_SNo (mul_SNo a x) HaxS)).
We prove the intermediate claim HyS: SNo y.
rewrite the current goal using Hydef (from left to right).
An exact proof term for the current goal is (SNo_div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b HnumS HbS).
We prove the intermediate claim Hbmul: mul_SNo b y = add_SNo c (minus_SNo (mul_SNo a x)).
rewrite the current goal using Hydef (from left to right).
rewrite the current goal using (mul_div_SNo_invR (add_SNo c (minus_SNo (mul_SNo a x))) b HnumS HbS Hb0) (from left to right).
Use reflexivity.
rewrite the current goal using (R2_xcoord_tuple x y) (from left to right).
rewrite the current goal using (R2_ycoord_tuple x y) (from left to right).
rewrite the current goal using Hbmul (from left to right).
We prove the intermediate claim HaxS2: SNo (mul_SNo a x).
An exact proof term for the current goal is HaxS.
We prove the intermediate claim HmAxS: SNo (minus_SNo (mul_SNo a x)).
An exact proof term for the current goal is (SNo_minus_SNo (mul_SNo a x) HaxS2).
rewrite the current goal using (add_SNo_assoc (mul_SNo a x) c (minus_SNo (mul_SNo a x)) HaxS2 HcS HmAxS) (from left to right).
rewrite the current goal using (add_SNo_com (mul_SNo a x) c HaxS2 HcS) (from left to right).
rewrite the current goal using (add_SNo_assoc c (mul_SNo a x) (minus_SNo (mul_SNo a x)) HcS HaxS2 HmAxS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv (mul_SNo a x) HaxS2) (from left to right).
An exact proof term for the current goal is (add_SNo_0R c HcS).
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) (x,y) HxyPlane Hprop).
∎