Prove a property of a function with a decEq in it

Question

It's easy to prove

f : Nat -> Nat

proveMe : (x : Nat) -> Maybe Nat
proveMe x = if (f x) == 0 then Just 42 else Nothing

theProof : (x : Nat) -> (f x = Z) -> (Just 42 = proveMe x)
theProof x prf = rewrite prf in Refl

But what if the calculation of Just 42 requires the proof that f x = 0?

proveMe2 : (x : Nat) -> Maybe Nat
proveMe2 x with (decEq (f x) Z)
    | Yes prf = Just 42
    | No _ = Nothing

theProof2 : (x : Nat) -> (f x = Z) -> (Just 42 = proveMe2 x)
theProof2 x prf = ?howToFillThis

How can I prove it now?

I tried to "follow the structure of the with clause", but when doing so I would have to convince idris that the contra-case is impossible:

theProof3 : (x : Nat) -> (f x = Z) -> (Just 42 = proveMe2 x)
theProof3 x prf with (decEq (f x) Z)
    | Yes prf2 = Refl
    | No contra impossible -- "...is a valid case"

Answer 1

I had completely forgotten about void : Void -> a. Using Ex falso quodlibet the proof is simply

theProof3 : (x : Nat) -> (f x = Z) -> (Just 42 = proveMe2 x)
theProof3 x prf with (decEq (f x) Z)
    | Yes prf2 = Refl
    | No contra = void $ contra prf