proposition: Lemma pow_odd_sgn : forall a b, 0<=b -> Odd b -> sgn (a^b) == sgn a.
proof: Proof. intros a b Hb H. destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. - apply sgn_pos. apply pow_pos_nonneg; trivial. - rewrite <- EQ'. rewrite pow_0_l. + apply sgn_0. + assert (b~=0) by (contradict H; now rewrite H, <-odd_spec, odd_0). order. - apply sgn_neg. rewrite <- (opp_involutive a). rewrite pow_opp_odd by trivial. apply opp_neg_pos. apply pow_pos_nonneg; trivial. now apply opp_pos_neg. Qed.
imports: Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow