proposition: Lemma BZ_idealS_abs a x: BZ_ideal x -> inc a x -> inc (BZabs a) x.
proof: Proof. move => pa pb. case /BZ_i0P: (proj31 pa _ pb) => az; last by rewrite (BZabs_pos az). by rewrite (BZabs_neg az); apply: BZ_idealS_opp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)