proposition: Theorem spec2_assoc p1 p2 p3 : is_generic p1 p2 -> is_tangent 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}// [p|]. 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||]; first 3 last. - move=> p3 x3 y3 e3 p5 x5 y5 e5 p6 x6 y6 e6 l1 -> -> _ _ x3Dx5 _ _ _ _ _ _. by case/and3P=> [_ /eqP[x3Ex5]]; case/eqP: x3Dx5. - by rewrite is_generic_inf. - by rewrite is_generic_inf. move=> p2 x2b y2b e2b p5 x5 y5 e5 l1 p2E p5E p5E1 y2bNZ l1E x5E y5E. rewrite [in p2 = _]p2E => [] [x2bE y2bE]. subst x2b y2b. elim/adde_case: (adde p1 p5) p1E p5E p5E1 => {p1 p5}// [p|p|]; last 3 first. - by rewrite is_generic_oppe. - by rewrite is_generic_irr. move=> p1 x1b y1b e1b p5b x5b y5b e5b p6 x6 y6 e6 l2 p1E p5bE p6E p6E1 x1bDx5b l2E x6E y6E. rewrite [in p1 = _]p1E [in p5b = _]p5bE => [] [x1bE y1bE] [x5bE y5bE]. subst x1b y1b x5b y5b => {p1E p5bE}// _ p4E1 _ _. elim/adde_case: (adde p4 p2) p2E p4E p4E1 => // [p|p|]. - by rewrite is_generic_oppe. - by rewrite is_generic_irr. move=> p4b x4b y4b e4b p3b x3b y3b e3b p7 x7 y7 e7 l3 p4bE p3bE p7E p7E1 x4bDx3b l3E x7E y7E. rewrite [in p3b = _]p3bE [in p4b = _]p4bE => [] [x3bE y3bE] [x4bE y4bE]. subst x3b y3b x4b y4b => {p3bE p4bE}// _ _ _. have x2Bx1NZ : x2 - x1 != 0 by rewrite subr_eq0 eq_sym. subst; apply: curve_elt_irr. field: e1 e2. apply/and5P; split => //. - apply: contra x4bDx3b => /eqP polE. rewrite -subr_eq0 (_ : 0 = 0 / -((x2 - x1) ^+ 2)); last by rewrite mul0r. apply/eqP; rewrite -polE; field. by rewrite oppr_eq0 sqrf_eq0 x2Bx1NZ. - by apply: K2D0. apply: contra x1bDx5b => /eqP polE. rewrite -subr_eq0 (_ : 0 = 0 / -((2%:R * y2) ^+ 2)); last by rewrite mul0r. apply/eqP; rewrite -polE; field. by rewrite oppr_eq0 sqrf_eq0 mulf_eq0 negb_or !y2bNZ !K2D0. field: e1 e2. apply/and5P; split => //. - apply: contra x4bDx3b => /eqP polE. rewrite -subr_eq0 (_ : 0 = 0 / -((x2 - x1) ^+ 2)); last by rewrite mul0r. apply/eqP; rewrite -polE; field. by rewrite oppr_eq0 sqrf_eq0 x2Bx1NZ. - by apply: K2D0. apply: contra x1bDx5b => /eqP x3E. rewrite -subr_eq0 (_ : 0 = 0 / -((2%:R * y2) ^+ 2)); last by rewrite mul0r. apply/eqP; rewrite -x3E; field. by rewrite oppr_eq0 sqrf_eq0 mulf_eq0 negb_or !y2bNZ !K2D0. Time Qed. Theorem spec3_assoc p1 p2 p3 : is_generic p1 p2 -> is_tangent p2 p3 -> is_generic (adde p1 p2) p3 -> is_tangent p1 (adde p2 p3) -> adde p1 (adde p2 p3) = adde (adde p1 p2) p3. Proof. elim/adde_case: (adde p1 p2) => {p1 p2}// [p|]. by rewrite is_generic_irr. intros 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 => [p|p|p||] {p2 p3} //; first 3 last. - move=> p2b x2b y2b e2b p3 x3 y3 e3 p5 x5 y5 e5 l2 p2bE p3E p3E1 p5E p5E1 l2E x5E y5E. rewrite [in p2b = _]p2bE => [] [x2bE y2bE] p4E1. subst x2b y2b; rewrite p2bE p3E => _ /and3P[_ /eqP[]x2Ex3 _]. by case/eqP : p5E1. - by rewrite is_generic_inf. - by rewrite is_tangent_oppe. move=> p2 x2b y2b e2b p5 x5 y5 e5 l1 p2E p5E p5E1 y2bNZ l1E x5E y5E p2E1 p4E1. rewrite p2E in p2E1; have [x2bE y2bE] := p2E1. subst y2b x2b => {p2E1}//. elim/adde_case: (adde p1 p5) p1E p4E1 p5E p5E1 => {p1 p5}// [p||]; first 2 last. - move=> p1b x1b y1b e1b p5b x5b y5b e5b p3 x3 y3 e3 l2 p1bE p5bE p3E p3E1. move=> x1bDx5b l2E x3E y3R. rewrite [in p1b = _]p1bE [in p5b =_]p5bE => [] [x1bE y1bE] p4E1 [x5bE y5bE]. subst x1b y1b x5b y5b => _ _ _ _ /and3P[_ /eqP] //. by rewrite p1bE p5bE => [] [x1Ex5]; case/eqP: x1bDx5b. - by rewrite is_tangent_oppe. intros p1 x1b y1b e1b p6 x6 y6 e6 l2 p1E p6E p6E1 y1bNZ l2E x6E y6E. rewrite ![in p1 = _]p1E => [] [x1bE y1bE] p4E1. subst x1b y1b => {p1E}//. case => x1E y1E; subst x5 y5. elim/adde_case: (adde p4 p2) p4E p4E1 p2E => // [p|p|]. - by rewrite is_generic_oppe. - by rewrite is_generic_irr. move=> p4b x4b y4b e4b p2b x2b y2b e2b1 p7 x7 y7 e7 l4 p4bE p2bE p7E p7E1 x4bDx2b l4E x7E y7E. rewrite [in p4b = _]p4bE [in p2b = _]p2bE => [] [x4bE y4bE] p4b1 [x2bE y2bE]. subst x4b y4b x2b y2b. pose pol := -(2%:R ^+ 2 * (2%:R * y2) ^+ 2) * ((3%:R * x2) * (4%:R * y2 ^+ 2) - (3%:R * x2 ^+ 2 + A) ^+ 2)^+2. pose pol1 := x2 * (4%:R * y2 ^+ 2) - ((3%:R * x2 ^+ 2 + A) ^+ 2 + - (2%:R * x2) * (4%:R * y2 ^+ 2)). have pol1NZ : pol1 != 0. apply: contra x1Dx2 => /eqP pol1E. rewrite -subr_eq0 (_ : 0 = 0 / -((2%:R * y2) ^+ 2)); last by rewrite mul0r. apply/eqP; rewrite -pol1E /pol1 x1E l1E; field. by rewrite oppr_eq0 sqrf_eq0 mulf_eq0 negb_or K2D0 y2bNZ. pose pol2 := 3%:R * x2 * (4%:R * y2 ^+ 2) - (3%:R * x2 ^+ 2 + A) ^+ 2. have pol2NZ : pol2 != 0. apply: contra x1Dx2 => /eqP polE. rewrite -subr_eq0 (_ : 0 = 0 / -((2%:R * y2) ^+ 2)); last by rewrite mul0r. apply/eqP; rewrite -polE x1E l1E /pol2; field. by rewrite oppr_eq0 sqrf_eq0 mulf_eq0 negb_or K2D0 y2bNZ. move=> _ _ _ _ _; rewrite p6E p7E; apply: curve_elt_irr. rewrite !(x6E, x7E, l2E, l4E, y4E, x4E, x1E, y1E, l1E, lE). field: e2. rewrite K2D0; apply/and5P; split => //. apply: contra x4bDx2b => /eqP polE. rewrite -subr_eq0 (_ : 0 = 0 / pol); last by rewrite mul0r. apply/eqP; rewrite -polE x4E lE x1E y1E l1E /pol. field. rewrite y2bNZ K2D0; apply/and4P; split => //. have -> : 4%:R = 2%:R ^+ 2 :> K by rewrite expr2 -natrM. by rewrite !(oppr_eq0, mulf_eq0, negb_or, K2D0, y2bNZ). apply: contra_neq y1bNZ => polE. rewrite y1E l1E; apply/eqP. rewrite (_ : 0 = 0 / ((2%:R * y2) ^+ 3)); last by rewrite mul0r. apply/eqP; rewrite -polE. by field; rewrite y2bNZ K2D0. rewrite !(y6E, y7E, l2E, l4E, x6E, x7E, y4E, x4E, y1E, x1E, l1E, lE). field: e2. rewrite y2bNZ K2D0; apply/and5P; split => //. apply: contra x4bDx2b => /eqP polE. rewrite -subr_eq0 (_ : 0 = 0 / pol); last by rewrite mul0r. apply/eqP; rewrite -polE x4E lE x1E y1E l1E /pol. field. rewrite y2bNZ K2D0; apply/and4P; split => //. have -> : 4%:R = 2%:R ^+ 2 :> K by rewrite expr2 -natrM. by rewrite !(oppr_eq0, mulf_eq0, negb_or, K2D0, y2bNZ). apply: contra_neq y1bNZ => polE. rewrite y1E l1E; apply/eqP. rewrite (_ : 0 = 0 / ((2%:R * y2) ^+ 3)); last by rewrite mul0r. apply/eqP; rewrite -polE. by field; rewrite y2bNZ K2D0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)