proposition: Lemma w_seq_le_S k : w_seq k <= w_seq k.+1.
proof: Proof. rewrite /w_seq big_ord_recr /=. by rewrite ler_pMr 1?ltW ?a'_gt1 // prodr_gt0 // => i _. 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