proposition: Lemma sub_compare_mono_l p q r : q<p -> r<p -> (p-q ?= p-r) = (r ?= q).
proof: Proof. intros Hqp Hrp. case (compare_spec r q); intros H. - subst. apply compare_refl. - apply sub_lt_mono_l; trivial. - apply lt_gt, sub_lt_mono_l; trivial. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef