proposition: Lemma nbos_rec n: natp n -> n <> \0c -> nb_odd_sums n = csumb (chalf (csucc n)) (fun i =>(nb_odd_sums (n -c (csucc (cdouble i))))).
proof: Proof. move => nN nz. set m := (chalf (csucc n)). have mN: natp m by apply: NS_half; apply: NS_succ. have mp i: inc i m <-> natp i /\ (csucc (cdouble i)) <=c n. suff: natp i -> (inc i m <-> csucc (cdouble i) <=c n). move => h; split => hyp. by move: (NS_inc_nat mN hyp) => iN; split => //; apply/(h iN). by move:hyp => [iN hyp]; apply/(h iN). move => iN. have ha: inc i m <-> csucc i <=c m. split; first by move/(NltP mN); move/(cleSltP iN). by move/(cleSltP iN); move/(NltP mN). apply: (iff_trans ha). have dsiN: natp (csucc (cdouble i)) by apply: NS_succ; apply: NS_double. apply: iff_trans (cleSSP (CS_nat dsiN) (CS_nat nN)). rewrite - (double_succ iN). case: (cdouble_halfV (NS_succ nN)) => ->; rewrite -/m. exact: (iff_sym (double_monotone (NS_succ iN) mN)). split => h. move/(double_monotone (NS_succ iN) mN):h => q. by apply: (cleT q); apply: cleS; apply: (NS_double mN). by apply:(double_le_odd1 mN (NS_succ iN)). pose lasti i f := Vg f (cpred (domain f)) = i. pose lastis i := Zo (odd_seqs n) (lasti (csucc (cdouble i))). pose F := Lg m lastis. have md: mutually_disjoint F. apply: mutually_disjoint_prop; rewrite /F; aw => i j y im jm; bw => //. move => /Zo_hi qa /Zo_hi qb. move:(NS_inc_nat mN im)(NS_inc_nat mN jm) => iN jN. have ci: cardinalp (cdouble i) by apply: CS_nat; apply: NS_double. have cj: cardinalp (cdouble j) by apply: CS_nat; apply: NS_double. by apply: double_inj => //; apply: csucc_inj => //; rewrite - qa - qb. rewrite /nb_odd_sums. have ->: odd_seqs n = unionb F. rewrite /F; set_extens t; last first. by move/setUb_P; aw; move =>[y ym]; bw => // /Zo_S. move => ti; move /odd_seqsP: (ti) => [ost cst]. case: (equal_or_not (domain t) \0c) => dnz. by case:nz; rewrite - cst csum_trivial. move: (nbos_restr dnz ost); set r := restr _ _;move => [qa qb qc]. move: (half_odd qc); set i := (Vg t (cpred (domain t))) => iv. have iN: natp i by case: qc. have hiN: natp (chalf i) by apply: NS_half. have him: inc (chalf i) m. apply/mp; split => //; rewrite -iv - cst qb; apply: csum_Mle0; fprops. by apply /setUb_P; exists (chalf i); aw; bw => //; apply:Zo_i. rewrite (csum_pr4 md) /csumb /F;aw; congr csum; apply: Lg_exten. move => i im; bw => //. move/mp: im => [iN le1]. move: (cdiff_pr le1). move: (NS_diff (csucc (cdouble i)) nN). set p := _ -c _ ; move => pN pv. apply/card_eqP. exists (Lf (fun z => restr z (cpred (domain z))) (lastis i) (odd_seqs p)). pose j := csucc (cdouble i). have oj: oddp j. by apply: odd_succ_double. saw; apply: lf_bijective. - move => z /Zo_P [/odd_seqsP [qa qb] qc]. case: (equal_or_not (domain z) \0c) => duz. by case: nz; rewrite - qb csum_trivial. move:(nbos_restr duz qa); set r := restr _ _; move =>[ra rb rc]. apply/odd_seqsP; split => //. move: (@NS_in_suml (csum r) (csucc (cdouble i))); rewrite - qc - rb => ww. have rra: natp (csum z) by ue. have rrb: cardinalp (csum r) by rewrite /csum; fprops. move: qb; rewrite rb qc - pv csumC; apply: csum_eq2l => //. by apply: NS_succ; apply: NS_double. by apply: ww. - move => u v /Zo_P[ua ub]/Zo_P[va vb] sr. move/odd_seqsP: ua =>[[uc1 uc2 uc3] ud]. move/odd_seqsP: va =>[[vc1 vc2 vc3] vd]. case: (equal_or_not (domain u) \0c) => duz. by case: nz; rewrite - ud csum_trivial. case: (equal_or_not (domain v) \0c) => dvz. by case: nz; rewrite - vd csum_trivial. move: (cpred_pr uc2 duz) (cpred_pr vc2 dvz) => [qa qb][qc qd]. have dudv: domain u = domain v. by rewrite qb qd; move: (f_equal domain sr); aw; move ->. apply: fgraph_exten => // t tu. move: tu; rewrite qb (succ_of_nat qa) => /setU1_P; case => tt. move: (f_equal (Vg ^~ t) sr); bw => //; ue. by rewrite tt ub dudv vb. - move => y /odd_seqsP [qa qb]. move: qa => [qa1 qa2 qa3]. set x := y +s1 (J (domain y) (csucc (cdouble i))). have dx1: domain x = osucc (domain y). by rewrite /x; aw; rewrite domain_setU1. have dx: domain x = csucc (domain y). by rewrite dx1 succ_of_nat. have cpd: (cpred (domain x)) = domain y by rewrite dx cpred_pr1; fprops. have ndy: ~ inc (domain y) (domain y) by apply: Nat_decent. have qc: lasti (csucc (cdouble i)) x. by rewrite /lasti cpd /x setU1_V_out. have fgx: fgraph x by apply: fgraph_setU1. have ndx: natp (domain x) by rewrite dx; fprops. have axo: allf x oddp. move => t; rewrite dx1; case/setU1_P. by move => h; rewrite setU1_V_in //; apply: qa3. by move ->; rewrite setU1_V_out. have rrx: (restr x (domain y)) = y. by apply: fgraph_exten; aww => t tdy; bw => //; rewrite setU1_V_in. have xn: inc x (odd_seqs n). apply/odd_seqsP; split => //. by rewrite (induction_sum1 dx1) // rrx - cpd qc qb csumC pv. exists x; [ apply: Zo_i => // | ue]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)