1章 $1 例題4 以下c)を示せ。 c) M ⊆ M' ⇒ M ∪ N ⊆ M' ∪ N 、M ∩ N ⊆ M' ∩ N. 上記をcoq/SSReflectで解いてみる。 問題自体は中学生程度で見りゃ分かるだろう程度です。 でも、coqを使用すると大学教授クラスでも納得する証明ができる・・と思う。 ---------…