newbie: proof from assumption of inductively defined prop

Stream: new members

[Kevin Buzzard]

[moving to new members stream]. You could prove that ev n was decidable, and then use dec_trivial to decide it.

[Rob Lewis]

Proving decidability is the right way to do it in general, but for this example:

example : ¬ ev 7 :=
begin
  intro h,
  repeat {cases h with _ h}
end