proposition: Lemma sub_decr n m : m<n -> n-m < n.
proof: Proof. intros. apply add_lt_mono_r with m. rewrite sub_add; trivial. apply lt_add_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef