proposition: Theorem sub_succ_r p q : p - (succ q) = pred (p - q).
proof: Proof. unfold sub; rewrite sub_mask_succ_r, sub_mask_carry_spec. destruct (sub_mask p q) as [|[r|r| ]|]; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef