proposition: Lemma nrCC1_a6' : [0] [<] (b[*]Half) [^]2.
proof: Proof. apply pos_square. apply ap_wdr_unfolded with (ZeroR[*]Half). 2: apply cring_mult_zero_op. apply mult_rht_resp_ap; try assumption. apply pos_ap_zero. apply pos_half. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing