proposition: Lemma BZprod_1_inversion_more a b c: intp a -> intp b -> intp c -> a = a *z (b *z c) -> [\/ a = \0z, b = \1z | b = \1mz].
proof: Proof. move => az bz cz. rewrite - {1} (BZprod_1r az) => h. case: (equal_or_not a \0z) => anz;first by constructor 1. move: (BZprod_eq2l ZS1 (ZSp bz cz) az anz h) => h1; symmetry in h1. move: (BZprod_1_inversion_l bz cz h1) => [_]; case =>H; in_TP4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)