proposition: Lemma nbos_restr s (m:= cpred (domain s)) (r := restr s m): domain s <> \0c -> odd_seq s -> [/\ odd_seq r, csum s = csum r +c (Vg s m) & oddp (Vg s m)].
proof: Proof. move => ha [hb hc hd]. move: (cpred_pr hc ha); rewrite -/m; move =>[mN mv]. have dd: domain s = m +s1 m by rewrite mv (succ_of_nat mN). split. - rewrite /r; split;aww => t; aw => tm; bw => //. apply: hd. by rewrite dd; apply: setU1_r. - by rewrite (induction_sum1 dd (Nat_decent mN)). - by apply: hd; rewrite mv; apply: Nsucc_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)