proposition: Lemma Nint_M1 a b: natp b -> a <=c b -> sub (Nint a) (Nint b).
proof: Proof. by move=> bN ab; rewrite (NintE bN) (NintE (NS_le_nat ab bN)); case: ab. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)