Module Arithmetic

Set Implicit Arguments.
Require Import MyTactics.

Lemma le_succ:
  forall m n,
  m <= n ->
  S m <= S n.

Lemma gt_succ:
  forall m n,
  m > n ->
  S m > S n.

Hint Resolve le_succ gt_succ.

Lemma lt_a_fortiori:
  forall m n,
  m < n ->
  m < S n.