proposition: Theorem mk_lelt_in_rev: forall x1 y1 H1 l H, In (x1, y1) l -> In (@curve_elt x1 y1 H1) (mk_lelt l H).
proof: Proof. intros x1 y1 H1 l; elim l; simpl; auto. intros (x, y) l1 Hrec H; simpl; auto. intros [H2 | H2]; auto. left; apply curve_elt_irr; injection H2; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith