proposition: Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b.
proof: Proof. intros a b ?. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ. - reflexivity. - symmetry. now apply pow_opp_even. Qed.
imports: Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow