proposition: Theorem Zeven_Zpower_odd : forall b e, (0 <= e)%Z -> Z.even b = false -> Z.even (Zpower b e) = false.
proof: Proof. intros b e He Hb. destruct (Z_le_lt_eq_dec _ _ He) as [He'|He']. rewrite <- Hb. now apply Z.even_pow. now rewrite <- He'. Qed.
imports: Coq(ZArith Lia Zquot)