Let a, b, c and x be given.

Assume HaR: a ∈ R.

Assume HbR: b ∈ R.

Assume HcR: c ∈ R.

Assume HxR: x ∈ R.

Set f to be the term affine_line_R2_param_by_x a b c.

We prove the intermediate claim Hfx: apply_fun f x ∈ EuclidPlane.

An exact proof term for the current goal is (affine_line_R2_param_by_x_function_on a b c HaR HbR HcR x HxR).

We prove the intermediate claim Happ1: apply_fun (projection1 R R) (apply_fun f x) = (apply_fun f x) 0.

An exact proof term for the current goal is (projection1_apply R R (apply_fun f x) Hfx).

rewrite the current goal using Happ1 (from left to right).

rewrite the current goal using (affine_line_R2_param_by_x_apply a b c x HxR) (from left to right).

An exact proof term for the current goal is (tuple_2_0_eq x (div_SNo (add_SNo c (minus_SNo (mul_SNo a x))) b)).

∎