proposition: Lemma even_pow : forall a b, 0<b -> even (a^b) = even a.
proof: Proof. intros a b Hb. apply lt_ind with (4:=Hb). - solve_proper. - now nzsimpl. - clear b Hb. intros b Hb IH. nzsimpl; [|order]. rewrite even_mul, IH. now destruct (even a). Qed.
imports: Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow