proposition: Lemma BZprodBl x y z: intp x -> intp y -> intp z -> (y -z z) *z x = (y *z x) -z (z *z x).
proof: Proof. by move => xz yz zz; rewrite BZprodC (BZprodC y) (BZprodC z) BZprodBr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)