How to add "assumed true" statements in Coq

Link:: https://stackoverflow.com/q/68060895

Display all goals and responses

Question

I tried to add a definition of a natural number in CoqIDE.

Inductive nat : Set :=
| O: nat
| S: nat -> nat.

But I couldn't add this as "assumed true":

forall (n m: nat, S n = S m -> n = m).

How do I add this?

Answer

I'm not completely clear on what you want to do, but your formula is not syntactically correct. I believe you meant forall (n m: nat), S n = S m -> n = m (note the parenthesis' placement).

Your statement is actually provable, no need to assume it:

Lemma S_inj : forall (n m: nat), S n = S m -> n = m.forall n m : nat, S n = S m -> n = m
Proof.forall n m : nat, S n = S m -> n = m intros n m [=].n, m: nat
H0: n = m
n = m assumption. Qed.

The [=] intro pattern expresses the built-in injectivity of the S constructor.