proposition: Lemma BZ_of_gcd (n m: nat) : BZgcd (BZ_of_Z n) (BZ_of_Z m) = BZ_of_Z (gcdn n m).
proof: Proof. move: (dvdn_gcdr m n) (dvdn_gcdr n m); rewrite gcdnC => sa sb. have sc: forall p, (p %| n) -> (p %| m) -> p %| gcdn n m. by move => p s1 s2; rewrite dvdn_gcd s1 s2. have pa: inc (BZ_of_Z n) BZ by apply: BZ_of_Z_inc. have pb: inc (BZ_of_Z m) BZ by apply: BZ_of_Z_inc. apply: (proj2(BZgcd_prop3' pa pb));split => //. + apply:positive_non_zero1. + by apply /BZ_of_div. + by apply /BZ_of_div. move => w / BZ_of_Zp_surjective [t <-]. by move/BZ_of_div => ha /BZ_of_div hb; apply/BZ_of_div ; apply: sc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)