Suponha que eu já tenha provado algum teorema em coq, e depois quero apresentá-lo como uma hipótese na prova de outro teorema. Existe uma maneira sucinta de fazer isso?

A necessidade disso geralmente surge quando eu quero fazer algo como uma prova por casos. E eu descobri que uma maneira de fazer isso éassert a declaração do teorema e, em seguida, imediatamente provar isso, mas isso parece um pouco complicado. Por exemplo, tenho tendência a escrever coisas como:

Require Import Arith.EqNat.

Definition Decide P := P \/ ~P.

Theorem decide_eq_nat: forall x y: nat, Decide (x = y).
Proof.
  intros x y. remember (beq_nat x y) as b eqn:E. destruct b.
    left. apply beq_nat_eq. assumption.
    right. apply beq_nat_false. symmetry. assumption. Qed.

Theorem silly: forall x y: nat, x = y \/ x <> y.
Proof.
  intros x y.
  assert (Decide (x = y)) as [E|N] by apply decide_eq_nat.
    left. assumption.
    right. assumption. Qed.

Mas existe uma maneira mais fácil do que ter que digitar todo oassert [statement] by apply [theorem] coisa?