proposition: Lemma csum_to_increasing2 n p: natp n -> natp p -> lf_axiom (fun y=> (csum_to_increasing_fct y n p)) (graphs_sum_le (csucc p) n) (functions_incr_nat (csucc p) (csucc n)).
proof: Proof. move=> nN pN y ys. have spN := (NS_succ pN); have snN:= (NS_succ nN). move: (csum_to_increasing1 nN pN ys) => ta1. rewrite /csum_to_increasing_fct. have aa: (forall u, inc u (domain y)-> inc (Vg y u) (csucc n)). move: ys => /Zo_P [/gfunctions_P2 [pa pb pc ] pd] u udy. exact: (pc _ (inc_V_range pa udy)). move: ys => /(graphs_sum_leP _ nN) [dy fhy les alc]. set g:= Lf _ _ _ . have p1: function g by apply: lf_function. apply/(increasing_nat_prop spN snN); split. by apply /functionsP; split => //; rewrite /g;aw. move => i j leij lejs. have jsp: inc j (csucc p) by apply /NltP. have isp: inc i (csucc p) by apply /(NltP spN); apply: (cle_ltT leij lejs). rewrite /g ! LfV //. rewrite /csum_to_increasing_fun /csumb -/(restr _ _) -/(restr _ _). have sab := (proj33 (cleSS leij)). by rewrite - (double_restr _ sab); apply: (csum_increasing1); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)