CODEWITHSUNDEEP
coq
Arjun Viswanathan
Arjun Viswanathan

Reputation: 319

I'm looking for this lemma about the nat type

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

Answers (3)

larsr
larsr

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

Tom And.
Tom And.

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

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23622

This statement does not hold: substituting m = 0, the conclusion becomes n < n, a clear contradiction.

Upvotes: 3

Related Questions