proposition: Lemma w_lt3 : w < 3%:Q.
proof: Proof. rewrite w_val ltr_pdivrMr ?rat_of_Z_Zpos // -subr_gt0. have -> : 3%:Q * rat_of_Z (2 * 10 ^ 15) - rat_of_Z 5949909309448377 = rat_of_Z (3 * 2 * 10 ^ 15 - 5949909309448377). ring. by rewrite rat_of_ZEdef ltr0z. 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