proposition: Lemma pow_eq_0 : forall a b, 0<=b -> a^b == 0 -> a == 0.
proof: Proof. intros a b Hb. apply le_ind with (4:=Hb). - solve_proper. - rewrite pow_0_r. order'. - clear b Hb. intros b Hb IH. rewrite pow_succ_r by trivial. intros H. apply eq_mul_0 in H. destruct H; trivial. now apply IH. Qed.
imports: NZAxioms NZMulOrder