fact: Fixpoint pos_mask_sub (x y : Pos) {struct y} : Pos_mask := match x, y with | p~1, q~1 => pos_mask_double (pos_mask_sub p q) | p~1, q~0 => pos_mask_succ_double (pos_mask_sub p q) | p~1, 1 => IsPos p~0 | p~0, q~1 => pos_mask_succ_double (pos_mask_sub_carry p q) | p~0, q~0 => pos_mask_double (pos_mask_sub p q) | p~0, 1 => IsPos (pos_pred_double p) | 1, 1 => IsNul | 1, _ => IsNeg end with pos_mask_sub_carry (x y : Pos) {struct y} : Pos_mask := match x, y with | p~1, q~1 => pos_mask_succ_double (pos_mask_sub_carry p q) | p~1, q~0 => pos_mask_double (pos_mask_sub p q) | p~1, 1 => IsPos (pos_pred_double p) | p~0, q~1 => pos_mask_double (pos_mask_sub_carry p q) | p~0, q~0 => pos_mask_succ_double (pos_mask_sub_carry p q) | p~0, 1 => pos_mask_double_pred p | 1, _ => IsNeg end.
imports: Basics.Overture Basics.Tactics Basics.Decidable Spaces.Nat.Core