proposition: Lemma power_plus_leEq : forall n (x y:R), (0 < n) -> ([0][<=]x) -> ([0][<=]y) -> (x[^]n [+] y[^]n)[<=](x[+]y)[^]n.
proof: Proof. intros [|n] x y Hn Hx Hy. exfalso; auto with *. induction n. simpl. rstepl ([1][*](x[+]y)). apply leEq_reflexive. rename n into m. set (n:=(S m)) in *. apply leEq_transitive with ((x[^]n[+]y[^]n)[*](x[+]y)). apply shift_zero_leEq_minus'. change (x[^]S n) with (x[^]n[*]x). change (y[^]S n) with (y[^]n[*]y). rstepr (y[*]x[^]n[+]x[*]y[^]n). apply plus_resp_nonneg; apply mult_resp_nonneg; try apply nexp_resp_nonneg; try assumption. change ((x[+]y)[^]S n) with ((x[+]y)[^]n[*](x[+]y)). apply mult_resp_leEq_rht. apply IHn. unfold n; auto with *. apply plus_resp_nonneg; assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)