fact: Definition add x y := match x, y with | 0, y => y | x, 0 => x | pos x', pos y' => pos (x' + y') | pos x', neg y' => pos_sub x' y' | neg x', pos y' => pos_sub y' x' | neg x', neg y' => neg (x' + y') end.
imports: BinNums BinPos BinNat