proposition: Lemma BZ_is_ideal2 a b: intp a -> intp b -> BZ_ideal (BZ_ideal2 a b).
proof: Proof. move => az bz. split; first by move => x /Zo_P []. move => x y /Zo_P [xz [u [v [uz vz pa]]]] /Zo_P [yz [w [z [wz zz pb]]]]. move: (ZSs uz wz) (ZSs vz zz) => ha hb. apply /Zo_P; split; first by apply:ZSs. exists (u +z w), (v +z z); split => //. rewrite (BZprodDr az uz wz) (BZprodDr bz vz zz). rewrite BZsum_ACA; first (by rewrite -pa -pb);by apply: ZSp. move => x y /Zo_P [xz [u [v [uz vz pa]]]] yz. apply /Zo_P; split; first by apply:ZSp. exists (u *z y), (v *z y); split; try apply: ZSp => //. rewrite (BZprodA az uz yz) (BZprodA bz vz yz). by rewrite - (BZprodDl yz (ZSp az uz) (ZSp bz vz)) -pa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)