fact: Fixpoint Qpositive_c (p q n : nat) {struct n} : Qpositive := match n with | O => One | S n' => match p - q with | O => match q - p with | O => One | v => dL (Qpositive_c p v n') end | v => nR (Qpositive_c v q n') end end.