proposition: Lemma pow_odd_abs_sgn : forall a b, Odd b -> a^b == sgn a * (abs a)^b.
proof: Proof. intros a b H. destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. - nzsimpl. rewrite abs_eq; order. - rewrite <- EQ'. nzsimpl. destruct (le_gt_cases 0 b). + apply pow_0_l. assert (b~=0) by (contradict H; now rewrite H, <-odd_spec, odd_0). order. + now rewrite pow_neg_r. - rewrite abs_neq by order. rewrite pow_opp_odd; trivial. now rewrite mul_opp_opp, mul_1_l. Qed.
imports: Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow