fact: Fixpoint Qpositive_i (w : Qpositive) : nat * nat := match w with | One => (1, 1) | nR w' => match Qpositive_i w' with | (p, q) => (p + q, q) end | dL w' => match Qpositive_i w' with | (p, q) => (p, p + q) end end.