proposition: Lemma BZgcd_id a: intp a -> BZgcd a a = BZabs a.
proof: Proof. move => az; rewrite - (BZ_gcd_abs az az); set b := BZabs a. move: (BZabs_iN az) => bzp; move: (BZp_sBZ bzp) => bz. by rewrite - (BZ_gcd_unq bz bz bzp (BZ_in_ideal3 bz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)