## Stream: new members

### Topic: newbie: proof from assumption of inductively defined prop

#### Kevin Buzzard (Oct 17 2018 at 18:04):

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

#### Rob Lewis (Oct 17 2018 at 18:35):

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


Last updated: May 16 2021 at 21:11 UTC