Leanパズル【問題編】偶数長のリスト

ちょっとしたLeanパズルを出題します。

リストの長さが偶数であることを表す帰納的述語を以下のように定義したとします。

variable {α : Type}

/-- リストの長さが偶数であることを表す述語 -/
@[grind]
inductive EvenLength : List α → Prop
  | nil : EvenLength []
  | cons_cons {a b : α} {l : List α} (h : EvenLength l) :
    EvenLength (a :: b :: l)

このとき、上記で定義した述語が xs.length % 2 = 0 と同値であることを示しましょう。
以下の sorry の部分を埋めて証明を完成させてください。必要に応じて補題や補助的な定義などを追加しても構いません。

example (xs : List α) : EvenLength xs ↔ xs.length % 2 = 0 := by
  sorry

ヒント

example ではなくて theorem を使って良いのであれば、ちょっと簡単になります。theorem を使った場合は、明示的に再帰を使うことで帰納法の仮定を得ることができるからです。