proposition: Lemma remark_7_1 : (n.+1 - a i <= n %/ a i * a i)%N.
proof: Proof. by rewrite leq_subLR -mulSn ltn_ceil. Qed.
imports: ZArith mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp tactics binomialz floor arithmetics posnum rat_of_Z hanson_elem_arith hanson_elem_analysis