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