proposition: Corollary sum_aV_leqn n k : \sum_(0 <= i < k) n %/ a i <= n.
proof: Proof. case: n => [|n]; first by rewrite big1 // => i _; exact: div0n. case: k => [| k]; first by rewrite big_nil. exact/ltnW/suminv_lt1. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial