proposition: Lemma BZcoprime_diff a b: intp a -> intp b -> BZcoprime a b -> BZcoprime a (b -z a).
proof: Proof. move => az bz; rewrite /BZcoprime /BZdiff -(BZprod_m1r az). by rewrite -(BZgcd_rem az bz ZSm1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)