proposition: Lemma nbos_p1 s: odd_seq s -> domain s <=c csum s.
proof: Proof. move: s. suff: forall n, natp n -> forall s, domain s = n -> odd_seq s -> n <=c csum s. by move => H s sa; apply: (H (domain s)) => //; case: sa. apply: Nat_induction. move => s sa _. rewrite csum_trivial //; fprops. move => n nN Hrec s sdc sa. move: (@succ_nz n); rewrite - sdc => dnz. move: (nbos_restr dnz sa). set m := Vg _ _; set r := restr _ _; move => [ra -> [rb rc]]. have de: domain r = n by rewrite /r sdc (cpred_pr1 (CS_nat nN)); aw. move:(Hrec r de ra); rewrite sdc => /cleSS h. apply: (cleT h). rewrite csucc_pr4; fprops; apply: csum_Meqle. apply: (cge1 (CS_nat rb)); dneg mm; rewrite mm; apply: even_zero. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)