fact: Fixpoint Qpositive_to_positive_i (qp:Qpositive) : positive := match qp with | nR qp => xI (Qpositive_to_positive_i qp) | dL qp => xO (Qpositive_to_positive_i qp) | One => xH end.
imports: Coq(ZArith) Coq(Lia) QArithSternBrocot(Q_field)