fact: Fixpoint length_of_Qpositive_to_positive (qp : Qpositive) : positive := match qp with | One => 1%positive | dL qp' => Pos.succ (length_of_Qpositive_to_positive qp') | nR qp' => Pos.succ (length_of_Qpositive_to_positive qp') end.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)