proposition: Lemma pow_add_upper : forall a b c, 0<=a -> 0<=b -> 0<c -> (a+b)^c <= 2^(pred c) * (a^c + b^c).
proof: Proof. assert (aux : forall a b c, 0<=a<=b -> 0<c -> (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)). - intros a b c (Ha,H) Hc. rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'. rewrite <- !add_assoc. apply add_le_mono_l. rewrite !add_assoc. apply add_le_mono_r. destruct (le_exists_sub _ _ H) as (d & EQ & Hd). rewrite EQ. rewrite 2 mul_add_distr_r. rewrite !add_assoc. apply add_le_mono_r. rewrite add_comm. apply add_le_mono_l. apply mul_le_mono_nonneg_l; trivial. apply pow_le_mono_l; try split; order. - 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)*(2^(pred c) * (a^c + b^c))). * apply mul_le_mono_nonneg_l; trivial. now apply add_nonneg_nonneg. * rewrite mul_assoc. rewrite (mul_comm (a+b)). assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order'). assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l). assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order). rewrite EQ', <- !mul_assoc. apply mul_le_mono_nonneg_l. -- apply pow_nonneg; order'. -- destruct (le_gt_cases a b). ++ apply aux; try split; order'. ++ rewrite (add_comm a), (add_comm (a^c)), (add_comm (a*a^c)). apply aux; try split; order'. Qed.
imports: NZAxioms NZMulOrder