instance PiBase.instCardGeThreeOfCardGeFour {X : Type u} [h : CardGeFour X] : CardGeThree X

Theorem 430: 3 ≤ 4

theorem PiBase.Formal.T430 : P176 ≤ P175