proposition: Lemma lt_minus_O_lt : forall n m : nat, m < n -> 0 < n - m.
proof: Proof. intros n m H'. apply Nat.add_lt_mono_l with (p := m). rewrite (Nat.add_comm m (n - m)). rewrite Nat.sub_add; auto with arith. rewrite Nat.add_0_r; auto. Qed.
imports: Coq(Arith ArithRing)