proposition: Lemma BZ_gcd_abs a b: intp a -> intp b -> BZgcd (BZabs a) (BZabs b) = BZgcd a b.
proof: Proof. move => az bz. by rewrite (BZ_gcd_abs1 az (ZSa bz)) (BZ_gcd_abs2 az bz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)