proposition: Lemma BZ_idealS_diff a b x: BZ_ideal x -> inc a x -> inc b x -> inc (a -z b) x.
proof: Proof. move => ix ax bx; rewrite /BZdiff. apply (proj32 ix _ _ ax (BZ_idealS_opp ix bx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)