proposition: Lemma coprime_sump a b k: natp k -> coprime a b -> coprime a (b +c (a *c k)).
proof: Proof. move => kN [aN bN cp]. have ha:= (NS_prod aN kN); have hb := NS_sum bN ha. split => // => x xda xds; apply:cp => //. rewrite csumC in xds. by have hc:= (cdivides_trans2 kN xda); move:(cdivides_diff1 bN hc xds). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)