proposition: Theorem add_casew: forall P, (forall p, P inf_elt p p) -> (forall p, P p inf_elt p) -> (forall p, P p (opp p) inf_elt) -> (forall p1 x1 y1 H1 p2 x2 y2 H2 p3 x3 y3 H3 l, p1 = (@curve_elt x1 y1 H1) -> p2 = (@curve_elt x2 y2 H2) -> p3 = (@curve_elt x3 y3 H3) -> p3 = add p1 p2 -> p1 <> opp p2 -> ((x1 = x2 /\ y1 = y2 /\ l = (3 * x1 * x1 + A) / (2 * y1)) \/ (x1 <> x2 /\ l = (y2 - y1) / (x2 - x1)) ) -> x3 = l ^ 2 - x1 - x2 -> y3 = -y1 - l * (x3 - x1) -> P p1 p2 p3)-> forall p q, P p q (add p q).
proof: Proof. intros; apply add_case; auto. intros; eapply X2; eauto. rewrite H; simpl; intros tmp; case H4; injection tmp; apply Keq_opp_is_zero. ring [H6]. intros; eapply X2; eauto. rewrite H; rewrite H0; simpl; intros tmp; case H6; injection tmp; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith