proposition: Lemma triangle : forall x y : CC, AbsCC (x[+]y) [<=] AbsCC x[+]AbsCC y.
proof: Proof. intros. elim x. intros x1 x2. elim y. intros y1 y2. unfold AbsCC in |- *. simpl in |- *. apply power_cancel_leEq with 2. auto. astepl ([0][+]ZeroR). apply plus_resp_leEq_both; apply sqrt_nonneg. astepl ([1][*](x1[+]y1)[*](x1[+]y1)[+][1][*](x2[+]y2)[*](x2[+]y2)). rstepr (sqrt ([1][*]x1[*]x1[+][1][*]x2[*]x2) (cc_abs_aid _ x1 x2)[^]2[+] sqrt ([1][*]y1[*]y1[+][1][*]y2[*]y2) (cc_abs_aid _ y1 y2)[^]2[+] Two[*]sqrt ([1][*]x1[*]x1[+][1][*]x2[*]x2) (cc_abs_aid _ x1 x2)[*] sqrt ([1][*]y1[*]y1[+][1][*]y2[*]y2) (cc_abs_aid _ y1 y2)). astepr ([1][*]x1[*]x1[+][1][*]x2[*]x2[+]([1][*]y1[*]y1[+][1][*]y2[*]y2)[+] Two[*]sqrt ([1][*]x1[*]x1[+][1][*]x2[*]x2) (cc_abs_aid _ x1 x2)[*] sqrt ([1][*]y1[*]y1[+][1][*]y2[*]y2) (cc_abs_aid _ y1 y2)). apply shift_leEq_rht. rstepr (Two[*] (sqrt ([1][*]x1[*]x1[+][1][*]x2[*]x2) (cc_abs_aid _ x1 x2)[*] sqrt ([1][*]y1[*]y1[+][1][*]y2[*]y2) (cc_abs_aid _ y1 y2)[-] (x1[*]y1[+]x2[*]y2))). apply mult_resp_nonneg. apply less_leEq. apply pos_two. apply shift_leEq_lft. apply power_cancel_leEq with 2. auto. apply mult_resp_nonneg; apply sqrt_nonneg. astepr (sqrt ([1][*]x1[*]x1[+][1][*]x2[*]x2) (cc_abs_aid _ x1 x2)[^]2[*] sqrt ([1][*]y1[*]y1[+][1][*]y2[*]y2) (cc_abs_aid _ y1 y2)[^]2). astepr (([1][*]x1[*]x1[+][1][*]x2[*]x2)[*]([1][*]y1[*]y1[+][1][*]y2[*]y2)). apply shift_leEq_rht. rstepr ((x1[*]y2[-]x2[*]y1)[^]2). apply sqr_nonneg. Qed.
imports: CoRN.complex.CComplex