proposition: Lemma BZgcd_div a b (g:= (BZgcd a b)): intp a -> intp b -> a = g *z (a %/z g) /\ b = g *z (b %/z g).
proof: Proof. move => az bz; move: (BZgcd_prop1 az bz)=> [pa pb];move: (BZp_sBZ pa) => pc. move: (BZ_in_ideal1 az bz); rewrite - pb -/g. move => [] /funI_P [q qa qb] /funI_P [q' qa' qb']. split. apply: BZdvds_pr; rewrite qb; rewrite BZprodC;apply: (BZdvds_pr1 qa pc). apply: BZdvds_pr; rewrite qb'; rewrite BZprodC;apply: (BZdvds_pr1 qa' pc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)