proposition: Theorem curve_elt_irr1: forall x1 x2 y1 y2 H1 H2, x1 = x2 -> (x1 = x2 -> y1 = y2) -> @curve_elt x1 y1 H1 = @curve_elt x2 y2 H2.
proof: Proof. intros x1 x2 y1 y2 H1 H2 H3 H4. apply curve_elt_irr; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith