Mizar/本体部/proof

proof ～;
 ...
end;

---

すでに式が証明されている場合には以下のように省略することが出来る。
式 by ファイル名:ラベル名;

---

証明方法の流れとしては、次のパターンが考えられる。

流れ	記号	証明法
↓	∴	直接証明	式を証明 正しい理由が記述 ↓∴ゆえに、 結果式
↑	∵	仮定法(数学的帰納法、など)	式を証明 仮定式 ↑∵なぜならば、 正しい理由を記述

否定(対偶法、背理法、など)

式を証明
否定式を仮定
∴ゆえに
矛盾するので、式は正しい

---

∵

now ～;
 ...
end;

---

場合分けして証明するとき。

ラベル:条件式
now per case by ラベル;
 case ラベル1:式1;
  ...
 thus 命題;
 case ラベル2:式2;
  ...
 thus 命題;
end;

---

hereby ～;
 ...
end;

hereby = thus + now