Example of idempotent function and related proof

Idempotent.idr

interface Idempotent (action : stateType -> stateType) where
  law : (state : stateType) -> let u = action state in action u = u

IncFrom : Nat -> Nat -> Nat
IncFrom original state = case decEq state original of
  Yes _ => S state
  No _ => state

{o : Nat} -> Idempotent (IncFrom o) where
  law s with (decEq s o)
    _ | Yes p with (decEq (S s) o) | (p)
      _ | No _ | Refl = Refl
    _ | (No p) = rewrite snd $ decEqContraIsNo p in Refl