proposition: Lemma add_lt_mono_l p q r : q<r <-> p+q < p+r.
proof: Proof. unfold lt. rewrite add_compare_mono_l. apply iff_refl. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef