proposition: Lemma w_gt1 : 1 < w.
proof: Proof. rewrite w_val ltr_pdivlMr ?rat_of_Z_Zpos // 1?mul1r -subr_gt0. by rewrite -rmorphB rat_of_Z_Zpos. 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