The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, Jul 03, 2013 at 10:24:14AM -0700, t x wrote:
> assert ( _statement_ ) as H0 by _tactic_ .
> pose proof (lemma ... H0 ...).

In ssreflect this could be expressed as

  have tmp : _statement_ by _tactic_.
  have {tmp} := lemma ... tmp ... .

where {tmp} is the syntax for clear, and have := is the anonymous
cut resulting in a new implication on top of your goal.

I see more compact ways only if know what you want to do with "lemma".
For example, if lemma proves an equality and you want to rewrite with it
you could even do that

  have -> := lemma ... (_ : _statement_) ...; last by _tactic_.

or

  rewrite (lemma ... (_ : _statement_) ...); last by _tactic_.

that follows Pierre's idea of using type inference to open a new goal.

Cheers
-- 
Enrico Tassi