proposition: Corollary suminv_lt1 i n : 0 < n -> \sum_(0 <= j < i) n %/ a j < n.
proof: Proof. case: n => [| n] // _; case: i => [| i]; first by rewrite big_nil. suff : ((\sum_(0 <= j < i.+1) n.+1 %/ a j)%N%:Q < n.+1%:Q)%R. by rewrite -ltz_nat ltr_int. suff hdiv : (\sum_(0 <= i0 < i.+1) (n.+1%:Q / (a i0)%:Q) < n.+1%:Q)%R. apply: le_lt_trans hdiv; rewrite sumMz; apply: ler_sum => j _. rewrite ler_pdivlMr // -intrM ler_int; exact: leq_trunc_div. rewrite -mulr_sumr gtr_pMr; last exact: ltr0z. exact: lt_sum_aV_1. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial