fact: Definition eq_elt p1 p2 := if p1 is @curve_elt x1 y1 _ then if p2 is @curve_elt x2 y2 _ then (x1 == x2) && (y1 == y2) else false else if p2 is @curve_elt x2 y2 _ then false else true.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)