proposition: Lemma BZgcd_prop1 a b: intp a -> intp b -> (inc (BZgcd a b) BZp /\ BZ_ideal1 (BZgcd a b) = BZ_ideal2 a b).
proof: Proof. move => az bz. set p := (fun z => BZ_ideal1 z = BZ_ideal2 a b). have pa: singl_val2 (inc^~ BZp) p. rewrite /p;move => x y /= pa e1 pb e2;apply: (BZ_ideal_unique_gen1 pa pb); ue. move:(BZ_is_ideal2 az bz)=> idax. have neid: nonempty (BZ_ideal2 a b). move: (proj1 (BZ_in_ideal1 az bz)) => pb; ex_tac. move: (BZ_principal idax neid) => [c ca cb]. move: (select_uniq pa ca cb); rewrite /p -/(BZgcd a b) => <-;split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)