proposition: Theorem add_case: 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 l, p1 = (@curve_elt x1 y1 H1) -> p2 = (@curve_elt x2 y2 H2) -> p2 = add p1 p1 -> y1<>0 -> l = (3 * x1 * x1 + A) / (2 * y1) -> x2 = l ^ 2 - 2 * x1 -> y2 = - y1 - l * (x2 - x1) -> P p1 p1 p2) -> (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 -> 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 P H1 H2 H3 H4 H5 p q; case p; case q; auto. intros x2 y2 e2 x1 y1 e1; unfold add. repeat ksplit. replace (@curve_elt x2 y2 e2) with (opp (@curve_elt x1 y1 e1)); auto; simpl. apply curve_elt_irr; auto; ring [KD0]. assert (HH: y1 <> 0). apply (@add_zero_diff x1 x2 y1 y2); auto. replace (@curve_elt x2 y2 e2) with (@curve_elt x1 y1 e1); auto. eapply H4; eauto; simpl; repeat ksplit; try apply curve_elt_irr; auto. case HH; apply Keq_opp_is_zero; auto. apply curve_elt_irr; auto. case (@Kmult_integral (y1 - y2) (y1 + y2)); try intros HH1. ring [e1 e2 KD]. apply Keq_minus_eq; auto. case KD0; apply Keq_minus_eq; ring_simplify; auto. eapply H5; eauto; simpl; repeat ksplit. apply curve_elt_irr; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith