fact: Definition Q_eq (n m : Q) := match n, m with | Zero, Zero => true | Qpos n', Qpos m' => match Qpositive_eq_dec n' m' with | left h => true | right h => false end | Qneg n', Qneg m' => match Qpositive_eq_dec n' m' with | left h => true | right h => false end | _, _ => false end.