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