proposition: Lemma sub_mask_neg p q : p<q -> sub_mask p q = IsNeg.
proof: Proof. apply sub_mask_neg_iff'. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef