proposition: Lemma BZgcd_simp a b c: intp a -> intp b -> intp c -> BZcoprime a b -> BZgcd a (b *z c) = BZgcd a c.
proof: Proof. move => az bz cz cop. move: (BZ_Bezout_if_coprime az bz cop) => [x [y [xz yz etc]]]. move: (f_equal (fun z => z *z c) etc). rewrite (BZprod_1l cz) (BZprodDl cz (ZSp az xz)(ZSp bz yz)). rewrite - (BZprodA az xz cz) (BZprodC b) - (BZprodA yz bz cz). move: (ZSp xz cz); set u := (x *z c) => uz eq1. move: (BZgcd_prop3 az (ZSp bz cz) ) => [_ h]. move: (BZgcd_prop3 az cz) => [[pa pb pc] _]. rewrite - (BZabs_pos (ZpS_gcd az cz)); apply: h. split; first by exact. by apply: (BZdvds_trans2 bz pb). move=> t ta tb; apply: pc; [ exact | rewrite - eq1 ]. have p1: t %|z (a *z u) by exact (BZdvds_trans (BZdvds_pr1' uz az) ta). move: (ZSp az uz) => auz. have p2: t %|z (y *z (b *z c)). rewrite BZprodC; exact: (BZdvds_trans (BZdvds_pr1' yz (ZSp bz cz)) tb). exact (proj1 (BZdvd_and_sum p1 p2)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)