proposition: Lemma Nintco_wor: worder_on (Nint_co a) (Nint a).
proof: Proof. move: cle_wor => wo. have r: forall x, inc x (Nint a) -> x <=c x. move=> x xi; move: (Nint_S1 xi) => xN; fprops. by move: (wordering_pr wo r). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)