Reputation: 319
I'm looking for this lemma about nats. I'm hoping it already exists in one of the Coq libraries so I don't have to prove it.
forall m n : nat, (S m < n)%nat -> (n - (S m) < n)%nat
Please point me to the library if it exists. Thanks!
Upvotes: 0
Views: 118
Reputation: 5811
You are almost looking for Nat.sub_lt
. I recommend using the Search
command to find lemmas. It's quite powerful.
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.
or auto using Nat.sub_lt, Nat.lt_le_incl, Nat.lt_0_succ.
or auto with arith.
Upvotes: 3
Reputation: 125
As far as I know, there is no Coq library to prove your statement. So you can come up with your own proof as:
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.
Upvotes: 0
Reputation: 23622
This statement does not hold: substituting m = 0
, the conclusion becomes n < n
, a clear contradiction.
Upvotes: 3