proposition: Lemma Nint_coP x: (inc x (interval_co Nat_order a b) <-> (a <=N x /\ x <N b)).
proof: Proof. rewrite/ Nat_lt/interval_co (proj2 Nat_order_wor); split. by move /Zo_P => [xb []] /Nat_order_leP pa [] /Nat_order_leP pb xnb. move => [pa [pb pc]]; apply /Zo_i; first by move: pa => [_]. by split; [| split => // ];apply /Nat_order_leP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)