proposition: Lemma orthonormalP S : reflect (uniq S /\ {in S &, forall phi psi, '[phi, psi]_G = (phi == psi)%:R}) (orthonormal S).
proof: Proof. rewrite orthonormalE; have [/= normS | not_normS] := allP; last first. by right=> [[_ o1S]]; case: not_normS => phi Sphi; rewrite /= o1S ?eqxx. apply: (iffP (pairwise_orthogonalP S)) => [] [uniqS oSS]. split=> // [|phi psi]; first by case/andP: uniqS. by have [-> _ /normS/eqP | /oSS] := eqVneq. split=> // [|phi psi Sphi Spsi /negbTE]; last by rewrite oSS // => ->. by rewrite /= (contra (normS _)) // cfdot0r eq_sym oner_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)