The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Jun 8, 2015 at 9:01 AM, Lars Rasmusson <Lars.Rasmusson AT sics.se> wrote:

Thanks a lot, Adam and Jonathan!

You could also use a version of the lemma that's transparent so it can be computed with:

Lemma mult_n_O_transparent :

  forall n:nat, 0 = n * 0.

Proof.

induction n.

+ reflexivity.

+ assumption.

Defined.  (* Note Defined. instead of Qed. *)

Lemma fobar: eq_refl = mult_n_O_transparent 1.

Proof.

reflexivity.

Qed.

(That might get unmanageable with more complex sets of lemmas from the standard library, though.)

-- 

Daniel Schepler