proposition: Lemma Ninto_wor: worder_on (Nint_cco a b) (Nintcc a b).
proof: Proof. move: cle_wor => wo. have r: (forall x, inc x (interval_cc Nat_order a b) -> x <=c x). move=> x xb; exact (cleR (CS_nat (Nint_S xb))). by move: (wordering_pr wo r). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)