proposition: Lemma Ninto_gleP x y: gle (Nint_cco a b) x y <-> [/\ inc x (Nintcc a b), inc y (Nintcc a b) & x <=c y].
proof: Proof. apply: graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)