仮説として前に証明された定理を紹介する

Question

すでにcoqで定理が証明されており、後で別の定理の証明として仮説として導入したいとします。これを行う簡潔な方法はありますか？

私は、事例による証明のようなことをしたいときに、これは一般的に私のために必要です。そして私は、これを行う方法の1つがassertの定理のステートメントであることを発見した後すぐに証明しますが、これは扱いにくいようです。たとえば、私はのようなもの書く傾向がある：

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. 

をしかし全体assert [statement] by apply [theorem]ものを入力するよりも簡単な方法はありますか？

Answer 1

pose proof theorem_name as X.を入力できます。Xは、紹介したい名前です。

---

あなたはすぐにそれを破壊するつもりなら、あなたもすることができます：destruct (decide_eq_nat x y).