proposition: Lemma BZ_in_ideal4 a: intp a -> (BZ_ideal (BZ_ideal1 a) /\ inc a (BZ_ideal1 a)).
proof: Proof. move=> az; rewrite (BZ_in_ideal3 az); split; first by apply: BZ_is_ideal2. apply: (proj1 (BZ_in_ideal1 az az)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)