proposition: Lemma coprime_sum a b: coprime a b -> coprime a (b +c a).
proof: Proof. move => h; move:(h) => [aN bN _]. rewrite -{2}(cprod1r (CS_nat aN)); apply:(coprime_sump NS1 h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)