proposition: Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b.
proof: Proof. intros a b (c,H). rewrite H. destruct (le_gt_cases 0 c). - rewrite 2 pow_mul_r by order'. rewrite 2 pow_2_r. now rewrite mul_opp_opp. - assert (2*c < 0) by (apply mul_pos_neg; order'). now rewrite !pow_neg_r. Qed.
imports: Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow