proposition: Lemma nth_elt_monotone K n m: natp n -> sub K Nat -> n <c cardinal K -> m <c n -> (nth_elt K m) <c (nth_elt K n).
proof: Proof. move => nN KN nk mn. have mN:= (NS_lt_nat mn nN). apply: (proj44 (nth_set7 nN KN nk)). have ub:= (proj42 (nth_set7 mN KN (clt_ltT mn nk))). move /(cleSltP mN): mn => le1. exact:(nth_set_M nN le1 ub). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)