proposition: Lemma F24_b (n: nat): n > 0 -> \sum_(i<n.+1 | ~~ odd i) ( 'C(n, i)) = \sum_(i<n.+1 | odd i) ('C(n, i)).
proof: Proof. move => np. rewrite [X in _ = X] (_: _ = \sum_(i < n.*2.-1 | ~~ odd i) 'C(n, i)). rewrite big_mkcond [in X in _ = X ] big_mkcond /=. move: np; case :n => [// | n _]. case: n => [|m]; first by rewrite 3! big_ord_recl 2! big_ord0 /=. have -> : (m.+2).*2.-1 = m.+3 + ( (m.+2).*2.-1 - m.+3). symmetry;apply: subnKC; rewrite 2! doubleS -pred_Sn 3! ltnS. rewrite -addnn; apply : leq_addr. rewrite big_split_ord /= [in X in _ = _ + X] big1 ?addn0 //. move => i _; rewrite bin_small ? if_same //. by rewrite 3!addSn 3! ltnS leq_addr. transitivity (\sum_(i < n.*2 | odd i) 'C(n, i)). rewrite big_mkcond [in X in _ = X] big_mkcond /=. move: np; case :n => // m _. have -> : (m.+1).*2 = m.+2 + ( (m.+1).*2 - m.+2). symmetry;apply: subnKC; rewrite doubleS !ltnS -addnn; apply : leq_addr. rewrite big_split_ord /= [in X in _ = _ + X] big1 ?addn0 //. move => i _; rewrite bin_small ? if_same //. by rewrite addnC ! addnS ! ltnS; apply : leq_addl. transitivity (\sum_(i<n) ('C(n, i.*2.+1))). have pa: forall i: 'I_n, i.*2.+1 < n.*2. by move => [i] hi /=; rewrite -doubleS leq_double. have pb: forall i: 'I_(n.*2), i./2 < n. move: np; case n; move => // m _ [i] hi /=. move: hi; rewrite doubleS ltnS ltnS => lin. by move: (half_leq lin) => /=; rewrite uphalf_double. have pc: forall i: 'I_n.*2, odd i -> Ordinal (pa (Ordinal (pb i))) = i. move => i oi; apply ord_inj => /=. by rewrite -add1n - {2} (odd_double_half (nat_of_ord i)) oi. rewrite (reindex_onto (fun i => Ordinal (pa i)) _ pc). apply: congr_big => // i; apply /andP; split. by case:i => i lin //=; rewrite odd_double. apply /eqP; apply: ord_inj => /=; exact: uphalf_double. transitivity (\sum_(i < n) 'C(n, i.*2)); first by rewrite F24_a. have pa: forall i: 'I_n, i.*2 < n.*2.-1. move: np; case n; move => // m _ [i] hi. rewrite doubleS ltnS leq_double -ltnS //. have pb: forall i: 'I_(n.*2.-1), i./2 < n. move: np; case n; move => // m _ [i] hi /=. move: hi; rewrite doubleS ltnS ltnS => lin. by move: (half_leq lin) => /=; rewrite half_double. have pc: forall i: 'I_n.*2.-1, ~~odd i -> Ordinal (pa (Ordinal(pb i))) = i. move => i oi; apply ord_inj => /=. by rewrite - {2} (odd_double_half (nat_of_ord i)) (negbTE oi). symmetry;rewrite (reindex_onto (fun i => Ordinal (pa i)) _ pc). apply: congr_big => // i;apply /andP; split. by case:i => i lin //=; rewrite odd_double. apply /eqP; apply: ord_inj => /=; exact: half_double. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)