proposition: Lemma eq_eltP : Equality.axiom eq_elt.
proof: Proof. case => [[|x2 y2 e2]| x1 y1 e1 [|x2 y2 e2]] /=; try by apply: (iffP idP). apply: (iffP andP) => [[/eqP x1E /eqP x2E]| [-> ->]//]. by apply: curve_elt_irr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)