同じ事を

Isar で書くと

lemma
  fixes a b :: "real"
  shows "(a ≠ 0 ∨ a = 0 ∧ b = 0) = (∃x. a * x = b)" (is "?P = ?Q")
proof
  assume ?P
  moreover  
  have "a ≠ 0 ==> a * (b / a) = b"
    by auto
  moreover
  have "a = 0 ∧ b = 0 ==> ?Q"
    by auto
  ultimately
  show "?Q"
    by metis
next
  assume ?Q
  hence "a = 0 ==> b = 0"
    by auto
  thus ?P
    by auto
qed

といった具合です．