Could someone remind me of the typical way to write a lemma in the middle of a proof (the equivalent of have in Lean), I have been searching around but can't find the typical thing people do.

Coq has several proof/tactic languages that do this in different ways, I assume you mean plain Ltac: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.assert

`assert`

Thank you @Quinn !

There is a `have`

tactic in Coq as well, available as soon as you

```
Require Import ssreflect.
```

Toy examples of basic usage:

```
Require Import Psatz ssreflect.
Lemma example (n m : nat) : n <= 0 -> m <= n -> n * m = 0.
Proof.
intros le0n le0m.
have eqn0 : n = 0. (* basic *)
lia.
have foo (k : nat) : k + n = k by lia. (* the syntax is akin to that of the global Lemma command *)
have eqm0 : m = 0 by lia. (* ommit the dot is the proof is a one-liner *)
have -> : n * m = 0 by lia. (* in fact you can even use an intro pattern instead of the name for the local lemma, here to rewrite on the fly *)
lia.
Qed.
```

Last updated: Jun 18 2024 at 09:02 UTC