proposition: Lemma lt_iff_add p q : p < q <-> exists r, p + r = q.
proof: Proof. unfold "<". rewrite <- sub_mask_neg_iff, compare_sub_mask. destruct sub_mask; now split. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef