proposition: Lemma w_seq_gt0 k : 0 < w_seq k.
proof: Proof. by rewrite prodr_gt0 // => i _ ; exact:a'_gt0. 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