fact: Definition pos_mask_pred (p : Pos_mask) : Pos_mask := match p with | IsPos 1 => IsNul | IsPos q => IsPos (pos_pred q) | IsNul => IsNeg | IsNeg => IsNeg end.
imports: Basics.Overture Basics.Tactics Basics.Decidable Spaces.Nat.Core