proposition: Lemma sub_mask_pos_iff p q r : sub_mask p q = IsPos r <-> q + r = p.
proof: Proof. split. - apply sub_mask_add. - intros <-; apply sub_mask_add_diag_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef