proposition: Lemma BZ_gcd_unq a b g: intp a -> intp b -> inc g BZp -> BZ_ideal1 g = BZ_ideal2 a b -> g = (BZgcd a b).
proof: Proof. move => az bz gp idp. set p := (fun z => BZ_ideal1 z = BZ_ideal2 a b). have un: (forall x y, inc x BZp -> inc y BZp -> p x -> p y -> x = y). rewrite /p;move => x y pa pb e1 e2; apply: (BZ_ideal_unique_gen1 pa pb); ue. move:(BZgcd_prop1 az bz) => [pa pb]. exact (un _ _ gp pa idp pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)