title: Lean : Proof that \ not p \to (p \ to q) or similar false \to p
body: <p>I am new at lean - prover and I am trying to solve the examples on the <a href="https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html" rel="nofollow noreferrer">online tutorial</a>.</p>
  
  <p>I am stuck at this example and I need to prove that "false implies q" or something like that.
  My code is :</p>
  
  <pre><code>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
  </code></pre>
  
  <p>I do not think that defining hnpq can help because this proof is part of the (¬ p ∨ q) → (p → q).
  In set theory I think that false implies everything.</p>
  
  <p>Any suggestions or thoughts?</p>