proposition: Lemma nth_set_M K n m: natp n -> m <=c n -> sub (nth_elts K m) (nth_elts K n).
proof: Proof. move => nN mn. rewrite - (cdiff_pr mn). move:(NS_diff m nN); set k:= (n -c m) => kN. move:(NS_le_nat mn nN) => mN; move: k kN;clear n mn nN. apply: Nat_induction; first by rewrite (csum0r (CS_nat mN)). move => n nN hrec. rewrite (csum_nS _ nN) (nth_elts_succ _ (NS_sum mN nN)). apply /(sub_trans hrec) /subsetU2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)