proposition: Lemma trmx_sesqui : M^T = (-1) ^+ eps *: M ^ theta.
proof: Proof. rewrite [in LHS](sesquiP _) // -mul_scalar_mx trmx_mul. by rewrite tr_scalar_mx mul_mx_scalar map_trmx trmxK. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix mxalgebra vector falgebra ssrnum algC algnum) mathcomp(fieldext) mathcomp(vector)