proposition: Lemma BZ_idealS_opp a x: BZ_ideal x -> inc a x -> inc (BZopp a) x.
proof: Proof. move => [pa _ pb] ax; rewrite - (BZprod_m1r (pa _ ax)). exact: (pb _ _ ax ZSm1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)