proposition: Lemma nroot_I_nexp : forall n n_, nroot_I n n_[^]n [=] II.
proof: Proof. intros n on. unfold nroot_I in |- *. apply eq_transitive with (II[^] (n * n)). apply nexp_mult. elim (nroot_I_nexp_aux n); try assumption. intros m H. rewrite H. apply eq_transitive with (II[^] (4 * m) [*]II[^]1). apply eq_symmetric. apply nexp_plus. apply eq_transitive with ((II[^]4) [^]m[*]II). apply bin_op_wd_unfolded. apply eq_symmetric. apply nexp_mult. apply nexp_one. cut (II[^]4 [=] [1]); intros. apply eq_transitive_unfolded with ([1][^]m[*]II). apply bin_op_wd_unfolded. apply un_op_wd_unfolded. exact H0. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with ([1][*]II). apply bin_op_wd_unfolded. apply one_nexp. apply eq_reflexive_unfolded. apply one_mult. replace 4 with (2 * 2). apply eq_transitive_unfolded with ((II[^]2) [^]2). apply eq_symmetric_unfolded. apply nexp_mult. apply eq_transitive_unfolded with ( [--] ([1]:CC) [^]2). apply un_op_wd_unfolded. exact I_square'. apply eq_transitive_unfolded with (([1]:CC) [^]2). apply inv_nexp_two. apply one_nexp. auto with arith. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing