CODEWITHSUNDEEP
coq
domino
domino

Reputation: 99

How to prove n <= n + S m in coq?

I have the last subgoal to prove a theorem. and it's:

1 subgoal
b, d : nat
H : 0 <= b
H0 : 0 <= d
m : nat
H1 : 0 <= m
H2 : S m = d
______________________________________(1/1)
b <= b + S m

I think I need an assumption like n <= n + Sm for this. Anyone can help me out?? Thanks a lot!

Upvotes: 0

Views: 57

Answers (2)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23612

The lia tactic, which stands for "Linear Integer Arithmetic", can solve this and many similar goals. E.g.:

Require Import Lia.

Goal forall b m, b <= b + S m.
Proof. intros. lia. Qed.

Upvotes: 3

Meven Lennon-Bertrand
Meven Lennon-Bertrand

Reputation: 1286

This is lemma le_plus_l of the standard library. It might be a good time for you to get familiar with the Search command. It is very useful to find theorems, and quite powerful once you get the hand of it. Here for instance I simply used Search (?x <= ?x + _) and got exactly the thing you were looking for.

Upvotes: 1

Related Questions