Я ищу эту лемму о типе nat

Question

Я ищу эту лемму о нац.Я надеюсь, что он уже существует в одной из библиотек Coq, поэтому мне не нужно доказывать это.

forall m n : nat, (S m < n)%nat -> (n - (S m) < n)%nat

Пожалуйста, укажите мне библиотеку, если она существует.Спасибо!

Answer 1

Вы почти ищете Nat.sub_lt.Я рекомендую использовать команду Search для поиска лемм.Это довольно мощный.

Require Import Arith.
Goal forall m n, (S m < n)%nat -> (n - (S m) < n)%nat.
  intros.
  Search (_ - _ < _).
  apply Nat.sub_lt.
  Search (_ < _ -> _ <= _).
  apply Nat.lt_le_incl, H.
  Search (0 < S _).
  apply Nat.lt_0_succ.
Qed.

или auto using Nat.sub_lt, Nat.lt_le_incl, Nat.lt_0_succ. или auto with arith.

Answer 2

Это утверждение не имеет места: подставляя m = 0, вывод становится n < n, явное противоречие.

Answer 3

Насколько я знаю, нет библиотеки Coq для подтверждения вашего утверждения. Таким образом, вы можете придумать свое собственное доказательство как:

Require Import PeanoNat List.
Import Nat.

Goal(forall m n : nat, (S m < n)%nat -> (n - (S m) < n)%nat).
Proof.
induction m.
destruct n.
intros.
inversion H.
intros. simpl.
rewrite Nat.sub_0_r.
apply lt_succ_diag_r.
intros.
intuition.
Qed.