我已成功在Linux（Ubuntu 17.04）中安装了Coq 8.6和CoqIDE。然而，我不知道如何继续添加SSReflect和MathComp到这个安装中。我查看的所有参考资料都对我来说很混乱。有人有一个简单的方法吗？ 我已经安装了opam。

我正在尝试处理 ssreflect 中的规范结构。这里有两段代码，我从这个地方获取。 我将提供布尔值和选项类型的代码片段。 Section BoolFinType. Lemma bool_enumP : Finite.axiom [:: true; false]. Proof. by...