proposition: Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b<0 \/ (0<b /\ a==0).
proof: Proof. intros a b. split. - intros H. destruct (lt_trichotomy b 0) as [Hb|[Hb|Hb]]. + now left. + rewrite Hb, pow_0_r in H; order'. + right. split; trivial. apply pow_eq_0 with b; order. - intros [Hb|[Hb Ha]]. + now rewrite pow_neg_r. + rewrite Ha. apply pow_0_l'. order. Qed.
imports: NZAxioms NZMulOrder