【Coq】コンピューターで証明しよう【コック】©2ch.net

[0029 片山博文MZ ◆T6xkBnTXz7B0 2015/01/27(火) 20:07:13.17 ID:SJxzPcnV]

>>26
訂正。ガラケーで入力大変。

(誤)
apply Z.mul_sub_distr_l.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.

(正)
apply Z.mul_sub_distr_l.
omega.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.