proposition: Lemma sqrt_I_nexp : sqrt_I[^]2 [=] II.
proof: Proof. apply eq_transitive with (sqrt_I[*]sqrt_I). apply nexp_two. unfold sqrt_I in |- *. apply eq_transitive with ((sqrt_Half[*]sqrt_Half[-]sqrt_Half[*]sqrt_Half) [+I*] (sqrt_Half[*]sqrt_Half[+]sqrt_Half[*]sqrt_Half)). apply eq_reflexive_unfolded. cut (sqrt_Half[*]sqrt_Half [=] Half); intros. apply eq_transitive with ([0][+I*] (Half[+]Half)). apply I_wd. apply cg_minus_correct. apply bin_op_wd_unfolded. exact H. exact H. apply eq_transitive with ([0][+I*][1]). apply I_wd. apply eq_reflexive. apply half_2. apply eq_reflexive. apply eq_transitive with (sqrt_Half[^]2). apply eq_symmetric. apply nexp_two. apply sqrt_sqr. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing