proposition: Lemma BZgcd_prop3' a b: intp a -> intp b -> (BZgcdp_prop a b (BZgcd a b) /\ forall g, BZgcdp_prop a b g -> (BZgcd a b) = g).
proof: Proof. move => az bz. move:(ZpS_gcd az bz) => hb. move: (BZgcd_prop3 az bz) => [[pa pb pc] pd]. have pr t: inc t BZp -> t %|z a -> t %|z b -> t %|z BZgcd a b. by move => ta tb tc; apply: pc. split; first done. move => g [gp ga gb gc]. suff: BZgcd_prop a b g by move/pd; rewrite BZabs_pos. suff : forall t, t %|z a -> t %|z b -> t %|z g by split. move => t ta tb. move: (ta) => [_ tu _]. case /BZ_i1P: (tu) => tp. + by move: ta tb; rewrite tp; apply: gc; apply:ZpS0. + by apply: gc => //; apply:BZps_sBZp. + move:(BZopp_negative1 tp) => otp. move/(BZdvds_opp1 _ tu): ta => ta1. move/(BZdvds_opp1 _ tu): tb => tb1. apply/(BZdvds_opp1 _ tu); exact: (gc _ (BZps_sBZp otp) ta1 tb1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)