proposition: Lemma BZgcd_prop3 a b: intp a -> intp b -> (BZgcd_prop a b (BZgcd a b) /\ forall g, BZgcd_prop a b g -> (BZgcd a b) = BZabs g).
proof: Proof. move => az bz. move: (ZS_gcd az bz) => gz. move: (BZgcd_div az bz) (ZS_quo az gz)(ZS_quo bz gz) => [pa pb] sa sb. set G := BZgcd a b. have r1:G %|z a by rewrite pa BZprodC;apply:(BZdvds_pr1 sa gz). have r2:G %|z b by rewrite pb BZprodC;apply:(BZdvds_pr1 sb gz). have r3:forall u : Set, u %|z a -> u %|z b -> u %|z G. move => u ua ub; move: (ua) => [_ uz _]. move: (ZS_quo az uz) (ZS_quo bz uz) => paz pbz. rewrite /G;move: (BZgcd_prop2 az bz) => [x [y [xz yz ->]]]. move: (ZSp paz xz) (ZSp pbz yz) => qaz qbz. rewrite (BZdvds_pr ua) (BZdvds_pr ub) - (BZprodA uz paz xz). rewrite - (BZprodA uz pbz yz)- (BZprodDr uz qaz qbz) BZprodC. apply: (BZdvds_pr1 (ZSs qaz qbz) uz). split;first by split. move => g [gp1 gp2 gp3]. move: (extensionality (BZdvds_pr6' (gp3 _ r1 r2))(BZdvds_pr6' (r3 _ gp1 gp2))). move: (gp1)(r1) => [_ gZ _] [_ GZ _]. move=> et; rewrite (BZ_ideal_unique_gen gZ GZ et). by rewrite /G (BZabs_pos (ZpS_gcd az bz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)