proposition: Lemma Pminus_mask_spec : forall p q, match Pminus_mask p q with | IsNul => Zpos p = Zpos q | IsPos k => Zpos p = q + k | IsNeg => p < q end.
proof: Proof. intros p q; case (Pos.sub_mask_spec p q). lia. all: intros r <-; lia. Qed.
imports: ZArith Lia