proposition: Lemma pow_pos_nonneg : forall a b, 0<a -> 0<=b -> 0<a^b.
proof: Proof. intros a b Ha Hb. apply le_ind with (4:=Hb). - solve_proper. - nzsimpl; order'. - clear b Hb. intros b Hb IH. nzsimpl; trivial. now apply mul_pos_pos. Qed.
imports: NZAxioms NZMulOrder