proposition: Lemma csum_to_increasing4 n p: natp n -> natp p -> injection (Lf (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; apply: lf_injective; first by apply: csum_to_increasing2. rewrite /csum_to_increasing_fct. move=> u v us vs h. move: (csum_to_increasing1 nN pN vs)=> ta2. have aux: forall x, inc x (csucc p) -> csumb (csucc x) (Vg u) = csumb (csucc x) (Vg v). move=> x xi; move: (f_equal (Vf ^~ x) h); rewrite !LfV//. by apply: csum_to_increasing1. clear h. move/Zo_S: (us) => /gfunctions_P2 /proj33 ru. move/Zo_S: (vs) => /gfunctions_P2 /proj33 rv. move /(graphs_sum_leP _ nN): us=> [du lesu fgu alcu]. move /(graphs_sum_leP _ nN): vs => [dv lesv fgv alcv]. apply: fgraph_exten =>//; first by ue. move=> x xdu. move: (ru _ (inc_V_range fgu xdu)) => xu. rewrite du - dv in xdu; move: (rv _ (inc_V_range fgv xdu)) => xv. move:(NS_inc_nat (NS_succ nN) xu) (NS_inc_nat (NS_succ nN) xv) => xuN xvN. rewrite dv in xdu; move: (aux x xdu). move: (NS_inc_nat (NS_succ pN) xdu) => xN. rewrite (csum_fs _ xN)(csum_fs _ xN). case: (equal_or_not x \0c)=> zx. by rewrite {1 3} zx ! csumb0 !Nsum0l. move /(NltP (NS_succ pN)): xdu => /proj1 le0. have le1: (csumb x (Vg v)) <=c csum v. move: (proj33 le0); rewrite - dv => xdv. by apply: csum_increasing1. have l1x:= (cge1 (CS_nat xN) zx). move: (cpred_pr6 pN l1x le0) =>[pa pb pc]. move: (NS_le_nat (cleT le1 lesv) nN) => sb. suff: csumb x (Vg u) = csumb x (Vg v) by move ->; apply: csum_eq2l. by rewrite pb; apply: aux; apply/(NleP pN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)