proposition: Lemma csum_to_increasing5 n p: natp n -> natp p -> surjection (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_surjective. by apply: csum_to_increasing2. have spN := (NS_succ pN); have snN:= (NS_succ nN). move =>y /(increasing_nat_prop spN snN) [/functionsP [fy sy ty] qb]. have rec:(forall u, u <> \0c -> inc u (csucc p) -> [/\ inc (cpred u) (csucc p), u = csucc (cpred u) & (Vf y (cpred u)) <=c (Vf y u)]). move=> u unz usy. move /(NltP (NS_succ pN)): (usy) => /proj1 le0. have uN := NS_inc_nat (NS_succ pN) usy. have l1u:= (cge1 (CS_nat uN) unz). move: (cpred_pr6 pN l1u le0) =>[pn sp pc]. have hu: inc (cpred u) (csucc p) by apply/NleP. have le1:= (cpred_le (CS_nat uN)). by split => //; apply: (qb _ _ le1); apply/NltP. pose f i := Yo(i= \0c) (Vf y \0c) ((Vf y i) -c (Vf y (cpred i))). have f1p: (forall i, inc i (csucc p) -> inc (f i) (csucc n)). move=> i i1; rewrite /f; Ytac h; first by rewrite -ty; Wtac; rewrite sy -h. move: (rec _ h i1) => [vsy usv wle]. rewrite - sy in i1 vsy. move:(Vf_target fy i1); rewrite ty ; move /(NleP nN) => win. apply /(NleP nN). exact: (cleT (cdiff_ab_le_a (Vf y (cpred i)) (proj31 win)) win). pose h i := csumb (csucc i) f. have H x: inc x (csucc n) -> cardinalp x by case/(NleP nN). have h1: forall i, inc i (csucc p) -> h i = Vf y i. move=> i /(NleP pN) ip; move: (NS_le_nat ip pN) => iN. rewrite/h/f;move: i iN ip; apply: Nat_induction. move => hh; rewrite succ_zero csumb1; Ytac0; rewrite card_card //. by apply/H; Wtac; rewrite sy; apply/(NleP pN); apply: cle0n. move=> m mN; rewrite /h => hr /(cleSltP mN) lmp. have smN: natp (csucc m) by fprops. have snz:= (@succ_nz m). have smsy: (inc (csucc m) (csucc p)) by apply/(NleP pN); apply/cleSltP. move: (rec _ snz smsy) => [vsy vp]. rewrite (csum_fs _ smN) /f (Y_false snz) (hr (proj1 lmp)). rewrite (cpred_pr1 (CS_nat mN)); apply: cdiff_pr. have p1: inc (Lg (csucc p) f) (graphs_sum_le (csucc p) n). apply /(graphs_sum_leP _ nN); split; aww. have pp:= (Nsucc_i pN). rewrite [csum _] (h1 _ pp); apply/(NleP nN); Wtac. hnf;aw. move => x xp; rewrite LgV//; exact: (H _ (f1p x xp)). rewrite/csum_to_increasing_fct; ex_tac. move :(csum_to_increasing1 nN pN p1) => aux. apply: function_exten; aw;trivial; first by apply: lf_function. rewrite sy; move=> x xsy /=; rewrite LfV// -(h1 _ xsy). apply: csumb_exten => t ts; rewrite LgV //; apply/(NleP pN). move/(NleP pN): xsy => l1; move/(NleP (NS_le_nat l1 pN)): ts => l2. apply:(cleT l2 l1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)