proposition: Lemma bin_mod2_sum_diag (f := fun n i => 'C(n.-1-i, i) %% 2) n: \sum_(i<n) (f n i) = fusc n.
proof: Proof. have Hu m: (m.*2.+1)./2 = m by exact:(half_bit_double m true). have Hv: forall n (i:'I_n), n.-1.+1 = n /\ i.*2 <= (n.-1).*2. move => k i; move:(prednK (leq_ltn_trans (leq0n i)(ltn_ord i))) => eq. by split => //; rewrite leq_double - ltnS eq (ltn_ord i). elim /fusc_ind: n. + by rewrite big_ord0. + by rewrite big_ord_recl big_ord0. + move => n H; rewrite fusc_even - H split_sum_even_odd1. suff ->: \sum_(i < n) f n.*2 i.*2.+1 = 0. rewrite addn0 /f; apply: eq_bigr => i _; move:(Hv n i) => [eq1 lt1]. by rewrite - {1} eq1 doubleS succnK subSn // - doubleB bin_mod2_prop2. apply: big1 => i _; rewrite /f; move:(Hv n i) => [eq1 lt1]. by rewrite - {1} eq1 doubleS succnK subSS- doubleB bin_mod2_prop1. + move => n Ha Hb; rewrite split_sum_even_odd fusc_odd Hu -Ha -Hb. rewrite -doubleS doubleK addnC /f; congr (_ + _);apply: eq_bigr => i _ /=. have [eq1 lt1] := (Hv n i). by rewrite -{1} eq1 doubleS subSn ?ltnS //subSS -doubleB bin_mod2_prop3. by rewrite -doubleB bin_mod2_rec2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)