CODEWITHSUNDEEP
coq
sana sobia
sana sobia

Reputation: 19

Checking the successor of natural number

I want to prove a goal and I have two hypothesis. Could you help me in proving the goal? Thank you very much for your help. Goal : (S m <? S m - (S m - 1)) = true with two hypothesis

m : nat
H : 1 < 1
H0 : (S  m =? 0) = false

Upvotes: 0

Views: 102

Answers (1)

HTNW
HTNW

Reputation: 29148

1 is not, in fact, less than 1. Therefore, we can prove absurdity. Good thing, too, since the goal itself is otherwise impossible.

Require Import PeanoNat.
contradict H. (* now proving ~(1 < 1) *)
(* Well, < is irreflexive: forall x, ~(x < x). *)
apply Nat.le_irrefl.

Upvotes: 2

Related Questions