proposition: Lemma pairwise_orthogonalP S : reflect (uniq (0 :: S) /\ {in S &, forall phi psi, phi != psi -> '[phi, psi] = 0}) (pairwise_orthogonal S).
proof: Proof. rewrite /pairwise_orthogonal /=; case notS0: (~~ _); last by right; case. elim: S notS0 => [|phi S IH] /=; first by left. rewrite inE eq_sym andbT => /norP[nz_phi /IH{}IH]. have [opS | not_opS] := allP; last first. right=> [[/andP[notSp _] opS]]; case: not_opS => psi Spsi /=. by rewrite opS ?mem_head 1?mem_behead // (memPnC notSp). rewrite (contra (opS _)) /= ?cfnorm_eq0 //. apply: (iffP IH) => [] [uniqS oSS]; last first. by split=> //; apply: sub_in2 oSS => psi Spsi; apply: mem_behead. split=> // psi xi /[!inE] /predU1P[-> // | Spsi]. by case/predU1P=> [-> | /opS] /eqP. case/predU1P=> [-> _ | Sxi /oSS-> //]. by apply/eqP; rewrite cfdotC conjC_eq0 [_ == 0]opS. 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)