proposition: Lemma finite_ordered_interval2 r: total_order r -> finite_set (substrate r) -> r \Is (Nint_co (cardinal (substrate r))).
proof: Proof. move => ha hb; have [f [isf _]] :=(finite_ordered_interval1 ha hb). by exists f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)