proposition: Lemma Ngcd_simp a b c: natp a -> natp b -> natp c -> Ncoprime a b -> Ngcd a (b *c c) = Ngcd a c.
proof: Proof. move => aN bN cN; rewrite /Ncoprime /Ngcd => h. move:(BZ_of_nat_i aN) (BZ_of_nat_i bN) (BZ_of_nat_i cN) => az bz cz. move: (BZp_hi_pr (ZpS_gcd az bz)); rewrite h => h1. by rewrite - (BZprod_cN bN cN) (BZgcd_simp az bz cz) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)