Angenommen, ich habe bereits einen Satz in coq bewiesen und möchte ihn später als Hypothese in den Beweis eines anderen Satzes einführen. Gibt es eine prägnante Möglichkeit, dies zu tun?

Das Bedürfnis danach entsteht normalerweise für mich, wenn ich so etwas wie einen Beweis für Fälle machen möchte. Und ich habe herausgefunden, dass ein Weg dies zu tun istassert die Aussage des Theorems, und beweisen Sie es dann sofort, aber das scheint irgendwie umständlich. Zum Beispiel neige ich dazu, Dinge zu schreiben wie:

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.

Aber gibt es einen einfacheren Weg, als das Ganze zu tippen?assert [statement] by apply [theorem] Ding?