Let a, b and c be given.

We prove the intermediate claim Heq: EuclidPlane = setprod R R.

Use reflexivity.

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

An exact proof term for the current goal is (affine_line_R2_subset a b c).

∎