proposition: Lemma csum_to_increasing1 y n p: natp n -> natp p -> inc y (graphs_sum_le (csucc p) n) -> lf_axiom (csum_to_increasing_fun y) (csucc p) (csucc n).
proof: Proof. move=> nN pN /(graphs_sum_leP _ nN) [dy dyxx les alc] u /(NleP pN) up. apply /(NleP nN); apply: cleT dyxx. apply: csum_increasing1; rewrite dy; exact: (proj33 (cleSS up)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)