proposition: Theorem spec1_assoc p1 p2 p3 : is_generic p1 p2 -> is_generic p2 p3 -> is_generic (adde p1 p2) p3 -> is_generic p1 (adde p2 p3) -> adde p1 (adde p2 p3) = adde (adde p1 p2) p3.
proof: Proof. elim/adde_case: (adde p1 p2) => {p1 p2} //. move=> p1 x1 y1 e1 p2 x2 y2 e2 l p1E p2E p2E1 y1NZ lE x2E y2E. by rewrite is_generic_irr. move=> p1 x1 y1 e1 p2 x2 y2 e2 p4 x4 y4 e4 l p1E p2E p4E p4E1 x1Dx2 lE x4E y4E. elim/adde_case: (adde p2 p3) p2E p4E1 => {p2 p3}// [p|p|p|]. - by rewrite is_generic_inf. - by rewrite is_generic_oppe. - by rewrite is_generic_irr. move=> p2 x2b y2b e2b p3 x3 y3 e3 p5 x5 y5 e5 l1 p2E. rewrite {}[in p2 = _]p2E. move=> p3E p5E p5E1 x2bDx3 l1E x5E y5E [x2bE y2bE] ; subst y2b x2b => {e2b}//. move: p1E p5E p5E1; elim/adde_case: (adde p1 p5) => {p1 p5}// [p|p|]. - by rewrite is_generic_oppe. - by rewrite is_generic_irr. move=> p1 x1b y1b e1b. move=> p5b x5b y5b e5b p6 x6 y6 e6 l2 p1E p5bE. rewrite {}[in p1 = _]p1E {}[in p5b = _]p5bE. move=> p6E _ x1bDx5b l2E x6E y6E [x1bE y1bE] [x5bE y5bE]; subst y1b x1b y5b x5b => {e1b e5b}// _ p4E1 _. elim/adde_case: (adde p4 p3) p3E p4E p4E1 => {p3 p4}// [p|p|]. - by rewrite is_generic_oppe. - by rewrite is_generic_irr. intros p4b x4b y4b H4b p3b x3b y3b e3b p7 x7 y7 H7 l3 p4bE p3bE p7E p7E1 x4bDx4b l3E x7E y7E. rewrite [in p3b = _]p3bE [in p4b = _]p4bE => [] [x3bE y3bE] [x4bE y4bE]. subst y3b x3b y4b x4b => {p3bE p4bE}// _ _ _ _. have x2Bx1NZ : x2 - x1 != 0 by rewrite subr_eq0 eq_sym. have x3Bx2NZ : x3 - x2 != 0 by rewrite subr_eq0 eq_sym. rewrite p6E p7E; apply: curve_elt_irr; subst. field: e1 e2 e3b => //. apply/and4P; split => //. apply: contra x4bDx4b=> /eqP x3E. rewrite -subr_eq0 (_ : 0 = 0 / -((x2 - x1) ^+ 2)); last by rewrite mul0r. apply/eqP; rewrite -x3E; field. by rewrite oppr_eq0 sqrf_eq0 x2Bx1NZ. apply: contra x1bDx5b => /eqP x3E. rewrite -subr_eq0 (_ : 0 = 0 / -((x3 - x2) ^+ 2)); last by rewrite mul0r. apply/eqP; rewrite -x3E; field. by rewrite oppr_eq0 sqrf_eq0 x3Bx2NZ. field: e1 e2 e3b => //. apply/and4P; split => //. apply: contra x4bDx4b => /eqP x3E. rewrite -subr_eq0 (_ : 0 = 0 / -((x2 - x1) ^+ 2)); last by rewrite mul0r. apply/eqP; rewrite -x3E; field. by rewrite oppr_eq0 sqrf_eq0 x2Bx1NZ. apply: contra x1bDx5b => /eqP x3E. rewrite -subr_eq0 (_ : 0 = 0 / -((x3 - x2) ^+ 2)); last by rewrite mul0r. apply/eqP; rewrite -x3E; field. by rewrite oppr_eq0 sqrf_eq0 x3Bx2NZ. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)