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