proposition: Theorem adde_shiftB p1 p2 p3 : adde p1 p2 = p3 -> p1 = adde p3 (oppe p2).
proof: Proof. move=> p1Dp2E; apply: addeI (_ : adde (oppe (oppe p2)) _ = _). rewrite ![adde (oppe (oppe _)) _]addeC. by rewrite addeK oppeK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)