fact: Definition lor a b := match a, b with | 0, _ => b | _, 0 => a | pos a, pos b => pos (Pos.lor a b) | neg a, pos b => neg (N.succ_pos (N.ldiff (Pos.pred_N a) (N.pos b))) | pos a, neg b => neg (N.succ_pos (N.ldiff (Pos.pred_N b) (N.pos a))) | neg a, neg b => neg (N.succ_pos (N.land (Pos.pred_N a) (Pos.pred_N b))) end.
imports: BinNums BinPos BinNat