proposition: Lemma nrCC1_c2pos : [0] [<] c2.
proof: Proof. unfold c2 in |- *. apply plus_resp_nonneg_pos. apply sqr_nonneg. apply pos_square. assumption. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing