proposition: Lemma nrCC1_a7_upper : [0] [<] b -> a'[*]b' [=] b[*]Half.
proof: Proof. intros. 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_nonneg. apply less_leEq. rstepl (ZeroR[*]Half). apply mult_resp_less. assumption. apply pos_half. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing