finally prove 'evenb n = negb (evenb (S n))'. just needed to destruct on strange match case. there's probably a simpler proof