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