Let a, b and c be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
Assume HcR: c ∈ R.
Let y be given.
Assume HyR: y ∈ R.
We will prove apply_fun (affine_line_R2_param_by_y a b c) y ∈ EuclidPlane.
rewrite the current goal using (affine_line_R2_param_by_y_apply a b c y HyR) (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 HdivReal: div_SNo c a ∈ real.
An exact proof term for the current goal is (real_div_SNo c HcReal a HaReal).
We prove the intermediate claim HdivR: div_SNo c a ∈ 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 (div_SNo c a) y HdivR HyR).
∎