proposition: Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0<c -> a^c + b^c <= (a+b)^c.
proof: Proof. intros a b c Ha Hb Hc. apply lt_ind with (4:=Hc). - solve_proper. - nzsimpl; order. - clear c Hc. intros c Hc IH. assert (0<=c) by order'. nzsimpl; trivial. transitivity ((a+b)*(a^c + b^c)). + rewrite mul_add_distr_r, !mul_add_distr_l. apply add_le_mono. * rewrite <- add_0_r at 1. apply add_le_mono_l. apply mul_nonneg_nonneg; trivial. apply pow_nonneg; trivial. * rewrite <- add_0_l at 1. apply add_le_mono_r. apply mul_nonneg_nonneg; trivial. apply pow_nonneg; trivial. + apply mul_le_mono_nonneg_l; trivial. now apply add_nonneg_nonneg. Qed.
imports: NZAxioms NZMulOrder