proposition: Lemma nrCC1_a'2pos : [0] [<] a'2.
proof: Proof. unfold a'2 in |- *. apply (mult_resp_pos IR). rstepr (c[-][--]a). apply shift_zero_less_minus. unfold c in |- *. apply sqrt_less'. unfold c2 in |- *. apply (Ccsr_wdl _ (cof_less (c:=IR)) (a[^]2[+][0]) (a[^]2[+]b[^]2)). apply plus_resp_less_lft. change ([0] [<] b[^]2) in |- *. apply pos_square. assumption. apply cm_rht_unit_unfolded. apply pos_half. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing