proposition: Lemma eq_peltP : Equality.axiom eq_pelt.
proof: Proof. case => x y z e [x1 y1 z1 e1]. apply: (iffP idP) => [/and3P[/eqP xE /eqP yE /eqP zE]| /= [/eqP -> /eqP -> /eqP ->]] //. by subst x y z; apply: curve_pelt_irr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)