proposition: Theorem spec1_assoc: forall p1 p2 p3, is_generic p1 p2 -> is_generic p2 p3 -> is_generic (add p1 p2) p3 -> is_generic p1 (add p2 p3) -> add p1 (add p2 p3) = add (add p1 p2) p3.
proof: Proof. intros p1 p2; kcase p1 p2. intros p p3 _ _ (HH, _); case HH; auto. intros p3 _ _ _ p4 _ _ _ _ _ _ _ _ _ _ _ p5 (_, (_, (HH, _))); case HH; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 p4 x4 y4 H4 l Hp Hp2 Hp4 Hp4b Hx Hl Hx4 Hy4 p3. generalize Hp2 Hp4b; clear Hp2 Hp4b; kcase p2 p3. intros; discriminate. intros p _ _ _ (_,(HH, _)); case HH; auto. intros p _ _ _ (_,(_,(_,HH))); case HH; rewrite opp_opp; auto. intros p2 _ _ _ p3 _ _ _ _ _ _ _ _ _ _ _ _ _ _ (_, (_, (HH, _))); case HH; auto. intros p2 x2b y2b H2b p3 x3 y3 H3 p5 x5 y5 H5 l1. intros Hp2; pattern p2 at 2; rewrite Hp2; clear Hp2. intros Hp3 Hp5 Hp5b Hd Hl1 Hx5 Hy5 tmp. injection tmp; intros; subst y2b x2b; clear tmp H2b. generalize Hp Hp5 Hp5b Hp4b H6 H9; clear Hp Hp5 Hp5b Hp4b H6 H9. kcase p1 p5. intros; discriminate. intros; discriminate. intros p _ _ _ _ _ (_,(_,(_,HH))); case HH; rewrite opp_opp; auto. intros p1 _ _ _ p5 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (_,(_,(HH,_))); case HH; auto. intros p1 x1b y1b H1b. intros p5b x5b y5b H5b p6 x6 y6 H6 l2. intros Hp1; pattern p1 at 2; rewrite Hp1; clear Hp1. intros Hp5; pattern p5b at 2; rewrite Hp5; clear Hp5. intros Hp6 _ Hd2 Hl2 Hx6 Hy6. intros tmp; injection tmp; intros HH1 HH2; subst y1b x1b; clear tmp H1b. intros tmp; injection tmp; intros HH1 HH2; subst y5b x5b; clear tmp H5b. intros _ Hp4b _ _. generalize Hp3 Hp4 Hp4b H7 H8; clear Hp3 Hp4 Hp4b H7 H8. kcase p4 p3. intros; discriminate. intros; discriminate. intros p _ _ _ _ (_, (_, (_,HH))); case HH; rewrite opp_opp; auto. intros p3 _ _ _ p4 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (_,(_,(HH, _))); case HH; auto. intros p4b x4b y4b H4b p3b x3b y3b H3b p7 x7 y7 H7 l3. intros Hp4b; pattern p4b at 2; rewrite Hp4b; clear Hp4b. intros Hp3b; pattern p3b at 2; rewrite Hp3b; clear Hp3b. intros Hp7 _ Hd3 Hl3 Hx7 Hy7. intros tmp; injection tmp; intros HH1 HH2; subst y3b x3b; clear tmp H3b. intros tmp; injection tmp; intros HH1 HH2; subst y4b x4b; clear tmp H4b. intros _ _ _. subst p6 p7; apply curve_elt_irr; clear H6 H7; apply Keq_minus_eq; clear H4 H5; subst. Time field [H1 H2 H3]; auto; repeat split; auto. intros VV; field_simplify_eq[H1 H2] in VV. case Hd3; symmetry; apply Keq_minus_eq; field_simplify_eq [H1 H2]; auto. intros VV; field_simplify_eq[H1 H2] in VV. case Hd2; symmetry; apply Keq_minus_eq; field_simplify_eq [H1 H2]; auto. Time field [H1 H2 H3]; auto; repeat split; auto. intros VV; field_simplify_eq[H1 H2] in VV. case Hd3; symmetry; apply Keq_minus_eq; field_simplify_eq [H1 H2]; auto. intros VV; field_simplify_eq[H1 H2] in VV. case Hd2; symmetry; apply Keq_minus_eq; field_simplify_eq [H1 H2]; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith