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