x y := match x, y with | 0, y => y | x, 0 => x | pos x', pos y' => pos (x' + y') | pos x', neg y' => binint_pos_sub x' y' | neg x', pos y' => binint_pos_sub y' x' | neg x', neg y' => neg (x' + y') end.
Require Import Basics. Require Import Spaces.Pos.Core.