Just a minor remark : QuantumLib.Complex.Cconj_opp uses a variable named capitalized C, which is unfortunate, since C is here the type of the complex numbers. Even if that doesn't prevent from using this lemma, could you rename this variable, for instance to uncapitalized c ? Currently, there's even more confusion when Check'ing Cconj_opp :
Check Cconj_opp.
(*Cconj_opp
: forall C0 : C, (- C0) ^* = - C0 ^*
*)
Actually, Coq noticed the name clash ... and displays instead C0, i.e the zero of complex numbers ! (I guess it has something to
do with C0 being a notation).