proposition: Lemma Nintco_gleP x y: gle (Nint_co a) x y <-> (x <=c y /\ y <c a).
proof: Proof. split. by move /graph_on_P1 => [] /(NintP aN) xa /(NintP aN) ya xy. move=> [xy ya]; move:(cle_ltT xy ya)=> h. by apply/graph_on_P1; split => //;apply /(NintP aN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)