fact: Definition land a b := match norm_pos a, norm_pos b with | Pos a, Pos b => Pos (NN.land a b) | Neg a, Pos b => Pos (NN.ldiff b (NN.pred a)) | Pos a, Neg b => Pos (NN.ldiff a (NN.pred b)) | Neg a, Neg b => Neg (NN.succ (NN.lor (NN.pred a) (NN.pred b))) end.
imports: ZArith Lia BigNumPrelude NSig ZSig