proposition: Lemma BZ_idealS_rem a b x: BZ_ideal x -> inc a x -> inc b x -> inc (a %%z b) x.
proof: Proof. move => ix ax bx; rewrite /BZrem; apply: (BZ_idealS_diff ix ax). exact: (proj33 ix _ _ bx (ZS_quo (proj31 ix _ ax) (proj31 ix _ bx))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)