proposition: Lemma add_compare_mono_r p q r : (q+p ?= r+p) = (q ?= r).
proof: Proof. rewrite 2 (add_comm _ p). apply add_compare_mono_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef