proposition: Lemma BZ_gcd_abs1 a b: intp a -> intp b -> BZgcd (BZabs a) b = BZgcd a b.
proof: Proof. move => uz vz; case /BZ_i0P: (uz) => su. by rewrite (BZabs_neg su) (BZgcd_opp uz vz). by rewrite (BZabs_pos su). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)