Let a, b, c and p be given.
Assume HaR: a ∈ R.
Assume HcR: c ∈ R.
Assume Hp: p ∈ setprod {div_SNo c a} R.
Set x0 to be the term div_SNo c a.
We prove the intermediate claim Hp0Sing: (p 0) ∈ {x0}.
An exact proof term for the current goal is (ap0_Sigma {x0} (λ_ : set ⇒ R) p Hp).
We prove the intermediate claim Hp1R: (p 1) ∈ R.
An exact proof term for the current goal is (ap1_Sigma {x0} (λ_ : set ⇒ R) p Hp).
We prove the intermediate claim Hp0eq: (p 0) = x0.
An exact proof term for the current goal is (singleton_elem (p 0) x0 Hp0Sing).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta {x0} R p Hp).
We prove the intermediate claim HpRR: p ∈ setprod R R.
We prove the intermediate claim HSingSub: {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).
We prove the intermediate claim Hx0R: x0 ∈ R.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is Hx0Real.
An exact proof term for the current goal is (singleton_subset x0 R Hx0R).
An exact proof term for the current goal is (setprod_Subq {x0} R R R HSingSub (Subq_ref R) p Hp).
We prove the intermediate claim Happ2: apply_fun (projection2 R R) p = p 1.
An exact proof term for the current goal is (projection2_apply R R p HpRR).
rewrite the current goal using Happ2 (from left to right).
rewrite the current goal using (affine_line_R2_param_by_y_apply a b c (p 1) Hp1R) (from left to right).
rewrite the current goal using Hp0eq (from right to left).
rewrite the current goal using Heta (from right to left).
Use reflexivity.
∎