proposition: Theorem curve_elt_irr x1 x2 y1 y2 e1 e2 : x1 = x2 -> y1 = y2 -> @curve_elt x1 y1 e1 = @curve_elt x2 y2 e2.
proof: Proof. move=> x1E y1E; move: e1 e2; rewrite x1E y1E => e1 e2. congr curve_elt. apply: Eqdep_dec.eq_proofs_unicity => x y. by case: (x =P y); [left | right]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)