prelude_aux: THEORY BEGIN x: VAR real y: VAR nonzero_real n: VAR nat i: VAR int even_plus1 : LEMMA even?(n) IFF NOT even?(n+1) even_plus : LEMMA even?(i) IFF NOT even?(i+1) even_int : LEMMA even?(n) IMPLIES integer_pred((n / 2)) not_even_int : LEMMA NOT even?(n) IMPLIES integer_pred(((n - 1) / 2)) even_m1_pow : LEMMA even?(i) IMPLIES (-1)^i = 1 not_even_m1_pow : LEMMA NOT even?(i) IMPLIES (-1)^i = -1 END prelude_aux