proposition: Lemma BZgcd_prodD a b c: intp a -> intp b -> inc c BZp -> (BZgcd (c *z a) (c *z b)) = c *z (BZgcd a b).
proof: Proof. move => az bz cp; move: (BZp_sBZ cp) => cz. move: (BZgcd_prop3 (ZSp cz az)(ZSp cz bz)). move => [_ sd]. move: (BZgcd_prop3 az bz) => [[sa sb sc] _]. set g := c *z BZgcd a b. move: (ZpS_gcd az bz) => gzp; move: (BZp_sBZ gzp) => gz. have ->: g = BZabs g. by rewrite /g (BZprod_abs cz gz) (BZabs_pos cp)(BZabs_pos gzp). case: (equal_or_not c \0z) => cnz. by rewrite /g cnz !BZprod_0l (BZgcd_zero ZS0). apply: sd;split. rewrite /g (BZprodC c) (BZprodC c). by move /(BZdvds_prod (ZS_gcd az bz) az cz cnz): sa. rewrite /g (BZprodC c) (BZprodC c). by move/(BZdvds_prod (ZS_gcd az bz) bz cz cnz): sb. move => u u1 u2; move: (BZdvds_pr u1) (BZdvds_pr u2). move: u1 => [_ uz _]. move: (ZS_quo (ZSp cz az) uz) (ZS_quo (ZSp cz bz) uz). set c1:= ((c *z a) %/z u) ; set c2 := ((c *z b) %/z u) => c1z c2z. move: (BZgcd_prop2 az bz) => [x [y [xz yz etc]]] e1 e2. rewrite /g etc (BZprodDr cz (ZSp az xz)(ZSp bz yz)). rewrite (BZprodA cz az xz)(BZprodA cz bz yz) e1 e2. rewrite -{1} (BZprodA uz c1z xz) - (BZprodA uz c2z yz). move: (ZSp c1z xz)(ZSp c2z yz) => qa qb; move: (ZSs qa qb) => qc. rewrite -(BZprodDr uz qa qb); apply (BZdvds_pr1' qc uz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)