proposition: Lemma Nint_coP1 x: (inc x (interval_co Nat_order a b) <-> (a <=c x /\ x <c b)).
proof: Proof. apply: (iff_trans (Nint_coP x)); split. by move=> [[_ _ pa] [[_ _ pb] pc]]. move=> [ax [bx xb]]; move:(NS_le_nat bx bN) => xN //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)