proposition: Lemma nrCC1_a7_lower : b [<] [0] -> a'[*][--]b' [=] b[*]Half.
proof: Proof. intros. apply eq_transitive_unfolded with ( [--] (a'[*]b')). apply cring_inv_mult_lft. cut (a'[*]b' [=] [--] (b[*]Half)); intros. rename H into H0. rename X into H. apply eq_transitive_unfolded with ( [--][--] (b[*]Half)). apply un_op_wd_unfolded. exact H0. apply cg_inv_inv. unfold a', b' in |- *. apply eq_transitive_unfolded with (sqrt (a'2[*]b'2) (less_leEq _ _ _ nrCC1_a6)). apply eq_symmetric_unfolded. apply NRootIR.sqrt_mult. apply eq_transitive_unfolded with (sqrt ((b[*]Half) [^]2) (less_leEq _ _ _ nrCC1_a6')). apply sqrt_wd. exact nrCC1_a5. apply sqrt_to_nonpos. apply less_leEq. rstepr (ZeroR[*]Half). apply mult_resp_less. assumption. apply pos_half. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing