fact: Definition spec_positive_fraction_encoding (a b : Z) (Ha : (0 < a)%Z) (Hb : (0 < b)%Z) := Qpositive_mult (Z_to_Qpositive a Ha) (Qpositive_inv (Z_to_Qpositive b Hb)).
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)