proposition: Theorem uniq_oppe p1 p2 : adde p1 p2 = inf_elt -> p2 = oppe p1.
proof: Proof. elim/adde_case: (adde p1 p2) => {p1 p2}// [p -> //||]. by move=> p1 x1 y1 e1 p2 x2 y2 e2 l _ ->. by move=> p1 x1 y1 e1 p2 x2 y2 e2 p3 x3 y3 e3 l _ _ ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)