Complex_Bounded_Operators: Various changes:
- Code generation support for explicit_cblinfun.
- Various changes and additions in Cblinfun_Matrix and Cblinfun_Code
- Lemma sandwich_compose: Switched lhs and rhs.
- New lemmas is_ortho_set_prod, ccsubspace_Times_ccspan.
- Definition cblinfun_inv: Default value 0 when inverse does not exist.
- Renamed riesz_frechet_representation_... -> riesz_representation_....
- Generalized lemma inj_ket.