proposition: Lemma nrCC1_a4 : (c[+]a) [*] (c[-]a) [=] b[^]2.
proof: Proof. apply eq_transitive_unfolded with (c[^]2[-]a[^]2). apply nexp_funny. unfold c in |- *. apply eq_transitive_unfolded with (c2[-]a[^]2). apply cg_minus_wd. apply sqrt_sqr. apply eq_reflexive_unfolded. unfold c2 in |- *. apply eq_transitive_unfolded with (a[^]2[+]b[^]2[+][--] (a[^]2)). apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (b[^]2[+]a[^]2[+][--] (a[^]2)). apply bin_op_wd_unfolded. apply cag_commutes_unfolded. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (b[^]2[+] (a[^]2[+][--] (a[^]2))). apply eq_symmetric_unfolded. apply plus_assoc_unfolded. apply eq_transitive_unfolded with (b[^]2[+][0]). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply cg_rht_inv_unfolded. apply cm_rht_unit_unfolded. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing