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