ガイド付き証明

証明チュートリアル

タクティクを1行ずつ入力してください。各行をカーネルが確認し、それまでのすべての証明状態を表示します。

現在の定理

定理を読み込んでいます…

0 タクティク
Enterで適用

証明状態の履歴

開始状態
最初の証明状態を準備しています…