proposition: Lemma Npower_plus_le_compat : forall a b c, c > 0 -> (a + b) ^ c >= a ^ c + b ^ c.
proof: Proof. induction c. intros. inversion H. intros. rewrite Npower_succ. rewrite Nat.mul_add_distr_r. apply Nat.add_le_mono. rewrite Npower_succ. apply Nat.mul_le_mono_l. destruct c. compute. auto. apply Nat.le_trans with (a^(S c)+b^(S c)). auto with arith. apply IHc. auto with arith. rewrite Npower_succ. apply Nat.mul_le_mono_l. destruct c. compute. auto. apply Nat.le_trans with (a^(S c)+b^(S c)). auto with arith. apply IHc. auto with arith. Qed.
imports: Arith Ntools Nle