For the definition and the theorem below
Inductive le : nat -> nat -> Prop :=
| le_n (n : nat) : le n n
| le_S (n m : nat) (H : le n m) : le n (S m).
Theorem Sn_le_Sm__n_le_m2 : forall n m,
S n <= S m -> n <= m.
Proof.
intros. remember (S n). remember (S m). induction H.
- subst. apply S_injective in Heqn1. subst. constructor.
- PROBELEM STATE
When we go to the problem state, the local context shown in CoqIDE is
n, m, n0 : nat
Heqn0 : n0 = S n
m0 : nat
Heqn1 : S m0 = S m
H : n0 <= m0
IHle : m0 = S m -> n <= m
I cannot understand why we get IHle : m0 = S m -> n <= m
. On my understanding, since the initial goal is forall n m, S n <= S m -> n <= m
, the induction hypothesis should be S n <= S m0 -> n <= m0
.
I would be much thankful if you could tell me why the induction hypothesis is not that in my mind.