proposition: Lemma triangle_IR : forall x y, AbsIR (x[+]y) [<=] AbsIR x[+]AbsIR y.
proof: Proof. intros. astepl (sqrt ((x[+]y) [^]2) (sqr_nonneg _ (x[+]y))). astepr (sqrt (x[^]2) (sqr_nonneg _ x) [+]sqrt (y[^]2) (sqr_nonneg _ y)). apply power_cancel_leEq with 2. auto. astepl ([0][+]ZeroR). apply plus_resp_leEq_both; apply sqrt_nonneg. astepl ((x[+]y) [^]2). rstepl (x[^]2[+]y[^]2[+]Two[*] (x[*]y)). rstepr (sqrt (x[^]2) (sqr_nonneg IR x) [^]2[+]sqrt (y[^]2) (sqr_nonneg IR y) [^]2[+] Two[*] (sqrt (x[^]2) (sqr_nonneg IR x) [*]sqrt (y[^]2) (sqr_nonneg IR y))). apply plus_resp_leEq_both. astepr (x[^]2[+]y[^]2). apply leEq_reflexive. apply mult_resp_leEq_lft. apply power_cancel_leEq with 2. auto. apply mult_resp_nonneg; apply sqrt_nonneg. rstepr (sqrt (x[^]2) (sqr_nonneg _ x) [^]2[*]sqrt (y[^]2) (sqr_nonneg _ y) [^]2). astepr (x[^]2[*]y[^]2). astepl (x[^]2[*]y[^]2). apply leEq_reflexive. apply less_leEq. apply pos_two. Qed.
imports: CoRN.reals.OddPolyRootIR