Making conclusions based on function output in idris

Question

Is there a way to draw a conclusion based on a the output of a function in Idris? For example let a function be defined as:

equalNumber: (x,y : Nat) -> Nat
equalNumber x y = case decEq x y of
                        Yes Refl => 42 
                        No contra => 0

Now i would really like to draw the conclusion that:

lemma : equalNumber x x = 42

Is this possible to prove? If it is: How?

Answer 1

Here is one solution:

total
lemma : equalNumber x x = 42
lemma {x} with (decEq x x)
  lemma {x} | (Yes Refl) = Refl
  lemma {x} | (No contra) = absurd $ contra Refl

Unfortunately, all my attempts to use decEqSelfIsYes lemma failed.