proposition: Lemma odd_seqsP n s: inc s (odd_seqs n) <-> odd_seq_for n s.
proof: Proof. split; first by move/Zo_hi. move=>h; apply:Zo_i => //. move: h => [[qa qb qc] qd]. apply/fgraphsP; split => //. by move => t tt; apply: (NS_inc_nat qb tt). by move => t /(range_gP qa) [x hb -> ]; move: (qc x hb); case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)