proposition: Lemma coprime3 a b c: coprime a b -> natp c -> a %|c (c *c b) -> a %|c c.
proof: Proof. move => cab cN dd; move: (cab) => [aN bN _]. move:(cdivides_pr dd). move:(NS_quo a (NS_prod cN bN)). set s := _ %/c _ => sN aav. case: (coprime_bezout2 cab). by move => [az bo]; move:dd; rewrite bo (cprod1r (CS_nat cN)). move => [u [v [uN vN bz]]]. move:(cdivides_pr1 (NS_prod uN cN) aN); rewrite cprodA bz cprodDl. rewrite (cprod1l (CS_nat cN)) cprodC cprodA aav - cprodA csumC => h. exact: (cdivides_diff1 cN (cdivides_pr1 (NS_prod sN vN) aN) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)