proposition: Lemma csum_Meqlt a a' b: natp b -> a <c a' -> (b +c a) <c (b +c a').
proof: Proof. move => bN la; move:b bN; apply: Nat_induction. by rewrite (csum0l (proj31_1 la)) (csum0l (proj32_1 la)). by move => n nN hr; rewrite (csum_Sn _ nN) (csum_Sn _ nN);apply: cltSS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)