proposition: Lemma abs_pow : forall a b, abs (a^b) == (abs a)^b.
proof: Proof. intros a b. destruct (Even_or_Odd b) as [H|H]. - rewrite pow_even_abs by trivial. apply abs_eq, pow_nonneg, abs_nonneg. - rewrite pow_odd_abs_sgn by trivial. rewrite abs_mul. destruct (lt_trichotomy 0 a) as [Ha|[Ha|Ha]]. + rewrite (sgn_pos a), (abs_eq 1), mul_1_l by order'. apply abs_eq, pow_nonneg, abs_nonneg. + rewrite <- Ha, sgn_0, abs_0, mul_0_l. symmetry. apply pow_0_l'. intro Hb. rewrite Hb in H. apply (Even_Odd_False 0); trivial. exists 0; now nzsimpl. + rewrite (sgn_neg a), abs_opp, (abs_eq 1), mul_1_l by order'. apply abs_eq, pow_nonneg, abs_nonneg. Qed.
imports: Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow