proposition: Lemma w_ge1 : 1 <= w.
proof: Proof. exact/ltW/w_gt1. 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