fact: Definition Qmult (x y : Q) := match x, y with | Qpos x', Qpos y' => Qpos (Qpositive_mult x' y') | Qpos x', Qneg y' => Qneg (Qpositive_mult x' y') | Qneg x', Qpos y' => Qneg (Qpositive_mult x' y') | Qneg x', Qneg y' => Qpos (Qpositive_mult x' y') | _, _ => Zero end.