proposition: Lemma nrCC4_a4 : [0] [<] y2.
proof: Proof. apply mult_cancel_pos_lft with (r[^]2[+][1]). apply odd_power_cancel_pos with n. assumption. apply (pos_wd _ _ _ y2_property). apply nrCC4_a2. apply less_leEq; apply nrCC4_a3. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing