proposition: Lemma BZ_of_coprime (n m: nat) : BZcoprime (BZ_of_Z n) (BZ_of_Z m) <-> (div.coprime n m).
proof: Proof. rewrite /div.coprime /BZcoprime BZ_of_gcd - BZ_Z_1n; split. by move/BZ_of_Z_injective;case; move => ->. by move /eqP => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)