Let a, b and c be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Let x be given.
Assume HxR: x ∈ R.
We will prove apply_fun (affine_line_R2_param_by_x a b c) x ∈ EuclidPlane.
rewrite the current goal using (affine_line_R2_param_by_x_apply a b c x HxR) (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 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 HdivReal: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b ∈ real.
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 HdivR: div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b ∈ R.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is HdivReal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b) HxR HdivR).
∎