proposition: Lemma sub_compare_mono_r p q r : p<q -> p<r -> (q-p ?= r-p) = (q ?= r).
proof: Proof. intros. rewrite <- (add_compare_mono_r p), 2 sub_add; trivial. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef