proposition: Lemma BZcoprime_add a b: intp a -> intp b -> BZcoprime a b -> BZcoprime a (a +z b).
proof: Proof. move => az bz; rewrite /BZcoprime. by rewrite -(BZgcd_rem az bz ZS1) (BZprod_1r az) BZsumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)