proposition: Lemma posrat (r : {posnum rat}) : 0 < ratr (num_of_pos r) :> R.
proof: Proof. by rewrite ltr0q. 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