proposition: Lemma nrCC_5a2 : forall n : nat, Nat.double n = 2 * n.
proof: Proof. intros. unfold Nat.double in |- *. unfold mult in |- *. auto with arith. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing