proposition: Lemma BZps_stable_prod1 a b: intp a -> intp b -> inc (a *z b) BZps -> ((inc a BZps <-> inc b BZps) /\ (inc a BZms <-> inc b BZms)).
proof: Proof. move => az bz. move:BZ_di_neg_spos => H. case /BZ_i1P: az. + by move => ->; rewrite BZprod_0l => /BZps_iP [_]. + case /BZ_i1P: bz. - by move => -> _; rewrite BZprod_0r => /BZps_iP [_] . - move => pa pb pc;split; split => // h; [case: (H _ h pb) | case:(H _ h pa)]. - move => pa pb pc;case: (H _ _ pc); exact (ZpmsS_prod pb pa). + case /BZ_i1P: bz. - by move => -> _; rewrite BZprod_0r => /BZps_iP [_]. - move => pa pb /H []; rewrite BZprodC; exact (ZpmsS_prod pa pb). - move => pa pb pc. split; split => // h; [case: (H _ pb h) | case: (H _ pa h)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)