fact: Fixpoint length_of_Qpositive (qp : Qpositive) : Z := match qp with | One => 0%Z | dL qp' => (1 + length_of_Qpositive qp')%Z | nR qp' => (1 + length_of_Qpositive qp')%Z end.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)