proposition: Lemma pow_add_r : forall a b c, 0<=b -> 0<=c -> a^(b+c) == a^b * a^c.
proof: Proof. intros a b c Hb. apply le_ind with (4:=Hb). - solve_proper. - now nzsimpl. - clear b Hb. intros b Hb IH Hc. nzsimpl; trivial. + rewrite IH; trivial. apply mul_assoc. + now apply add_nonneg_nonneg. Qed.
imports: NZAxioms NZMulOrder