proposition: Lemma AbsCC_strext : fun_strext AbsCC.
proof: Proof. unfold fun_strext in |- *. intros z1 z2 H. cut (AbsCC z1[^]2 [#] AbsCC z2[^]2). elim z1. intros x1 y1. elim z2. intros x2 y2. intro H'. assert (H'' : x1[^]2[+]y1[^]2 [#] x2[^]2[+]y2[^]2). astepl (AbsCC (x1[+I*]y1) [^]2). astepr (AbsCC (x2[+I*]y2) [^]2). assumption. cut (x1[^]2 [#] x2[^]2 or y1[^]2 [#] y2[^]2). intros H'''. elim H'''; intro H0. cut (x1 [#] x2). intro H1. simpl in |- *. unfold cc_ap in |- *. unfold Re, Im in |- *. left. assumption. apply (nexp_strong_ext IR 2). assumption. simpl in |- *. unfold cc_ap in |- *. simpl in |- *. right. apply (nexp_strong_ext IR 2). assumption. apply (bin_op_strext_unfolded _ _ _ _ _ _ H''). assert (H1 : AbsCC z1[-]AbsCC z2 [#] [0]). cut (AbsCC z1[-]AbsCC z2 [#] AbsCC z2[-]AbsCC z2). intro H0. astepr (AbsCC z2[-]AbsCC z2). assumption. apply minus_resp_ap_rht. assumption. assert (H2 : AbsCC z1[+]AbsCC z2 [#] [0]). apply Greater_imp_ap. assert (H0 : AbsCC z1 [#] [0] or [0] [#] AbsCC z2). apply ap_cotransitive_unfolded. assumption. elim H0. intro H'. assert (H'' : [0] [<] AbsCC z1). apply (AbsCC_ap_zero_imp_pos _ H'). apply leEq_less_trans with (y := AbsCC z2). apply AbsCC_nonneg. rstepl (AbsCC z2[+][0]). rstepr (AbsCC z2[+]AbsCC z1). apply plus_resp_less_lft. assumption. intro H'. assert (H'' : [0] [<] AbsCC z2). apply AbsCC_ap_zero_imp_pos. apply ap_symmetric_unfolded. assumption. apply leEq_less_trans with (y := AbsCC z1). apply AbsCC_nonneg. rstepl (AbsCC z1[+][0]). apply plus_resp_less_lft. assumption. cut (AbsCC z1[^]2[-]AbsCC z2[^]2 [#] [0]). intro H3. cut (AbsCC z1[^]2[-]AbsCC z2[^]2 [#] AbsCC z2[^]2[-]AbsCC z2[^]2). intro H4. rstepl (AbsCC z1[^]2[-]AbsCC z2[^]2[+]AbsCC z2[^]2). rstepr ([0][+]AbsCC z2[^]2). apply op_rht_resp_ap with (x := AbsCC z1[^]2[-]AbsCC z2[^]2) (y := ZeroR) (z := AbsCC z2[^]2). rstepr (AbsCC z2[^]2[-]AbsCC z2[^]2). assumption. rstepr ZeroR. assumption. astepl ((AbsCC z1[-]AbsCC z2) [*] (AbsCC z1[+]AbsCC z2)). apply mult_resp_ap_zero; assumption. Qed.
imports: CoRN.complex.CComplex