proposition: Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b.
proof: Proof. intros a b Ha. destruct (lt_ge_cases b 0) as [Hb|Hb]. - now rewrite !(pow_neg_r _ _ Hb). - apply le_ind with (4:=Hb). + solve_proper. + nzsimpl; order'. + clear b Hb. intros b Hb IH. nzsimpl; trivial. now apply mul_nonneg_nonneg. Qed.
imports: NZAxioms NZMulOrder