Let a, b, c and y be given.
Assume HaR: a ∈ R.
Assume HcR: c ∈ R.
Assume HyR: y ∈ R.
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 prove the intermediate claim Hx0R: x0 ∈ R.
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 Hx0Real: x0 ∈ real.
An exact proof term for the current goal is (real_div_SNo c HcReal a HaReal).
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hx0Real.
We prove the intermediate claim Hxy: (x0,y) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x0 y Hx0R HyR).
We prove the intermediate claim Happ2: apply_fun (projection2 R R) (x0,y) = (x0,y) 1.
An exact proof term for the current goal is (projection2_apply R R (x0,y) Hxy).
rewrite the current goal using Happ2 (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq x0 y).
∎