legacy_Complex_simps

[Lawrence Paulson]

Can anybody explain why all of the lemmas about the complex constructor “Complex" have been shoved into this lemma list, legacy_Complex_simps? 

There is seemingly a view to push users into writing complex expressions in the form x + iy, which looks nice in a mathematics textbook but is certain to complicate reasoning where the real and imaginary parts are dealt with separately.

Larry