Prove that a Cartan matrix cannot have eigenvalue 4

[ocfnash]

The task is to address the following TODO:

mathlib4/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean

Lines 346 to 348 in 88da430

	-- TODO Turn this `Fact` into a lemma: it is always true and may be proved via Perron-Frobenius
	-- See https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Eigenvalues.20of.20Cartan.20matrices/near/516844801
	variable [Fact ((4 - b.cartanMatrix).det ≠ 0)] [P.IsReduced] [P.IsIrreducible]

As noted there, some useful remarks are available on Zulip here