Coqの非構造的プルーフ？

Question

Coqで非定常的な方法で存在定理を証明できますか？具体的には、不合理な数があることを証明することを考えています。 x^yは合理的です。

Answer 1

この特定の証拠のために、除外された中間公理を仮定する必要があります。

Require Import Coq.Logic.Classical_Prop. 
About classic. 

をか（それはいくつかの注意が必要として、より高度な使用）自分では、いくつかの具体的な形でそれを追加します：あなたは、ライブラリからインポートすることができます。それにもかかわらず、標準ライブラリの実数はすでに古典的なので、この原則をそれらから導き出すことができます。