proposition: Lemma sub_mask_add p q r : sub_mask p q = IsPos r -> q + r = p.
proof: Proof. case sub_mask_spec; congruence. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef