Для определения и следующей теоремы
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
Когда мы переходим в состояние проблемы, локальный контекст, показанный в CoqIDE, является
n, m, n0 : nat
Heqn0 : n0 = S n
m0 : nat
Heqn1 : S m0 = S m
H : n0 <= m0
IHle : m0 = S m -> n <= m
Я не могу понять, почему мы получаем IHle : m0 = S m -> n <= m. Насколько я понимаю, поскольку исходная цель - forall n m, S n <= S m -> n <= m, гипотеза индукции должна быть S n <= S m0 -> n <= m0.
Я был бы очень благодарен, если бы вы могли сказать мне, почему гипотеза индукции не соответствует моему мнению.
