Pavel Shuhray (May 10 2023 at 06:21): Pavel Shuhray (May 10 2023 at 06:21):Hi
What is the names of the following theorems
forall n:nat, S n = 0 -> False.
forall (n,m:nat), S n = S m -> n = m.
How can I find them myself?
Laurent Théry (May 10 2023 at 06:30):Require Import Arith.
(* forall n:nat, S n = 0 -> False. *)
Search (S _ = 0).
(* forall (n,m:nat), S n = S m -> n = m. *)
Search (S _ = S _).
Note also that those properties are corollaries of the fact that S and 0 are constructors. So, you can also use the tactics discriminate and injection, respectively, instead of applying theorems.
Last updated: Oct 04 2023 at 19:01 UTC