proposition: Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b).
proof: Proof. intros a b (c,H). rewrite H. destruct (le_gt_cases 0 c) as [LE|GT]. - assert (0 <= 2*c) by (apply mul_nonneg_nonneg; order'). rewrite add_1_r, !pow_succ_r; trivial. rewrite pow_opp_even by (now exists c). apply mul_opp_l. - apply double_above in GT. rewrite mul_0_r in GT. rewrite !pow_neg_r by trivial. now rewrite opp_0. Qed.
imports: Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow