proposition: Lemma w_seq_incr k l : (k <= l)%N -> w_seq k <= w_seq l.
proof: Proof. elim: l => [|l ihl]; first by rewrite leqn0 => /eqP->. rewrite leq_eqVlt ltnS; case/predU1P => [-> // | /ihl hkl]. exact: le_trans (w_seq_le_S _). 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