fact: Definition decode_Q (q : Q) := match q with | Qpos p => (Z_of_nat (fst (Qpositive_i p)), Z_of_nat (snd (Qpositive_i p))) | Qneg p => ((- Z_of_nat (fst (Qpositive_i p)))%Z, Z_of_nat (snd (Qpositive_i p))) | Zero => (0%Z, 1%Z) end.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)