proposition: Theorem addeI p1 p2 p3 : adde p1 p2 = adde p1 p3 -> p2 = p3.
proof: Proof. elim/adde_casew : (adde p1 p2) => {p1 p2}// [p pE|p infE|]. - apply/sym_equal/(uniq_zeroe (_ : _ p)). by rewrite addeC. - by apply/sym_equal/uniq_oppe. move=> p1 x1 y1 e1 p2 x2 y2 e2 p4 x4 y4 e4 l p1E p2E p4E p4E1 p1DNp2 H x4E y4E. move: p1E p4E1 p1DNp2; rewrite p4E. elim/adde_casew : (adde p1 p3) => {p1 p3}// [p pE p4E1 pDNp2 p4E2|]. apply: uniq_zeroe (_ : _ = p). by rewrite -addeC -p4E1. move=> p1 x1b y1b e1b p3 x3 y3 e3 p5 x5 y5 e5 l'. move=> p1bE p3E p5E p5bE p1DNp3 H' x5E y5E p1E p4E1 p1DNp2 p4E2. rewrite p4E2 p5bE in p4E1. move: p1bE; rewrite p1E => [] [x1E y1E]; subst x1b y1b. move: (p4E2); rewrite p5E => [] [x4E1 y4E1]. rewrite p5bE in p4E2. have : (l' - l) * (x4 - x1) == 0. move: y5E; rewrite -{}x4E1 -y4E1 {}y4E => /eqP; rewrite -subr_eq0 => /eqP <-. apply/eqP; ring. (rewrite mulf_eq0 => /orP[]; rewrite subr_eq0 => /eqP) => [l'E|x4E2]. - move: x4E1; rewrite x4E x5E l'E => /subrI x2Ex3. have [] := curve_elt_oppe e2 e3 x2Ex3; first by rewrite p2E p3E. rewrite -p2E -p3E => p2E1. have [p1ENp1|/eqP p1DNp1] := p1 =P oppe p1. have [[x1E y1E lE]|[x1Dx2 lE]] := H. case/eqP: p1DNp3. rewrite -p2E1 p1E p2E. by apply: curve_elt_irr. rewrite lE in l'E. have [[x1E y1E l'E1]|[x1Dx3 l'E1]] := H'. case/eqP: p1DNp2; rewrite p2E1 oppeK. by rewrite p1E p3E; apply: curve_elt_irr. rewrite l'E1 in l'E. move: p2E1; rewrite p2E p3E => [] [x2E y2E]. apply: curve_elt_irr => //. subst x3 y2. apply/eqP; rewrite -subr_eq0; apply/eqP. move/eqP: l'E; rewrite -subr_eq0 => /eqP polE. rewrite (_ : 0 = 0 * (x1 - x2)); last by rewrite mul0r. by rewrite -polE; field; rewrite subr_eq0 eq_sym. rewrite -(oppeK p3) -p2E1. apply: addeI_oppe (_ : p1 != _) => //. by rewrite [in RHS]p2E1 oppeK. case: (curve_elt_oppe e4 e1); rewrite ?p4E2 -?p1E // => p1Dp3E. apply: etrans (_ : inf_elt = _); last apply: sym_equal; by apply: (uniq_zeroe (_ : _ = p1)); rewrite addeC // -p4E1. by apply: etrans (_ : adde (oppe p1) (oppe p1) = _); last apply: sym_equal; apply: adde_oppe_double_opp; rewrite -?p4E1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)