proposition: Lemma a_grows m n : m <= n -> a m <= a n.
proof: Proof. move/subnK<-; rewrite addnC; case: (n - m) => [| k]; first by rewrite addn0. exact/ltnW/a_grows2. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial