proposition: Lemma nrCC1_a5 : a'2[*]b'2 [=] (b[*]Half) [^]2.
proof: Proof. unfold a'2, b'2 in |- *. apply eq_transitive_unfolded with ((c[+]a) [*] (Half[*] ((c[-]a) [*]Half))). apply eq_symmetric_unfolded. apply mult_assoc_unfolded. apply eq_transitive_unfolded with ((c[+]a) [*] ((c[-]a) [*]Half[*]Half)). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply mult_commutes. apply eq_transitive_unfolded with ((c[+]a) [*] ((c[-]a) [*] (Half[*]Half))). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply mult_assoc_unfolded. apply eq_transitive_unfolded with ((c[+]a) [*] (c[-]a) [*] (Half[*]Half)). apply mult_assoc_unfolded. apply eq_transitive_unfolded with (b[^]2[*] (Half[*]Half)). apply bin_op_wd_unfolded. exact nrCC1_a4. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (b[*]b[*] (Half[*]Half)). apply bin_op_wd_unfolded. apply nexp_two. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (b[*]b[*]Half[*]Half). apply mult_assoc_unfolded. apply eq_transitive_unfolded with (b[*] (b[*]Half) [*]Half). apply bin_op_wd_unfolded. apply eq_symmetric_unfolded. apply mult_assoc_unfolded. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (b[*]Half[*]b[*]Half). apply bin_op_wd_unfolded. apply mult_commutes. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (b[*]Half[*] (b[*]Half)). apply eq_symmetric_unfolded. apply mult_assoc_unfolded. apply eq_symmetric_unfolded. apply nexp_two. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing