theorem-proving - 精益：证明 \not p \to (p \ to q) 或类似的 false \to p

Question

我是精益证明的新手，我正在尝试解决在线教程中的示例。

我被这个例子困住了，我需要证明“假暗示q”或类似的东西。我的代码是：

variables p q : Prop
example : ¬ p → (p → q) := 
    assume h : ¬ p,
    assume hp : p,
    --have hnpq : ¬ p ∨ q, from or.inl h,
    have hf : false, from h hp,
    --show q, from hf
    sorry

我不认为定义 hnpq 会有所帮助，因为这个证明是 (¬ p ∨ q) → (p → q) 的一部分。在集合论中，我认为 false 意味着一切。

有什么建议或想法吗？