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