proposition: Lemma add_le_mono p q r s : p<=q -> r<=s -> p+r <= q+s.
proof: Proof. intros. apply le_trans with (p+s). - now apply add_le_mono_l. - now apply add_le_mono_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef