proposition: Theorem uniq_zeroe p1 p2 : adde p1 p2 = p2 -> p1 = inf_elt.
proof: Proof. elim/adde_case: (adde p1 p2) => {p1 p2}//=; first by case. move=> p1 x1 y1 e1 p2 x2 y2 e2 l -> -> p2E y1NZ lE x2E y2E [x2E1 y2E1]. have : 2%:R * y1 == 0. by apply/eqP; rewrite -(subrr y2) [in - _]y2E y2E1 x2E1; ring. rewrite mulf_eq0 (negPf K2D0) => /eqP y1Z. by case/eqP: y1NZ. move=> p1 x1 y1 e1 p2 x2 y2 e2 p3 x3 y3 e3 l p1E p2E p3E p3E1 x1Dx2 lE x3E y3E. rewrite p2E p3E=> [] [x3E1 y3E1]. suff y2Z : y2 = 0. have /eqP[] := adde_aux1 e1 e2 x1Dx2 y2Z. by rewrite -lE -x3E. suff : 2%:R * y2 == 0. by rewrite mulf_eq0 (negPf K2D0) => /eqP. apply/eqP. have /eqP := y3E; rewrite x3E1 y3E1 lE -subr_eq0 => /eqP <-. by field; rewrite subr_eq0 eq_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)