fact: Definition mul x y := match x, y with | 0, _ => 0 | _, 0 => 0 | pos x', pos y' => pos (x' * y') | pos x', neg y' => neg (x' * y') | neg x', pos y' => neg (x' * y') | neg x', neg y' => pos (x' * y') end.
imports: BinNums BinPos BinNat