## Stream: Coq users

### Topic: intermediate goal in proof

#### Callan McGill (Jan 24 2022 at 19:09):

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.

#### Karl Palmskog (Jan 24 2022 at 19:11):

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`

#### Callan McGill (Jan 24 2022 at 19:12):

Thank you @Quinn !

#### Assia Mahboubi (Jan 25 2022 at 09:20):

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: Jan 29 2023 at 01:02 UTC