proposition: Lemma w_val : w = rat_of_Z 5949909309448377 / rat_of_Z (2 * 10 ^ 15).
proof: Proof. rewrite /w /a'0_ub /a'1_ub /a'2_ub /a'3_ub /a'4_ub. by field. 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