Shared finite, well-founded game theory

PDL completeness uses the game determinacy library already preserved with the GL coalgebra development. Its games, strategies, winners and determinacy theorem coincide with the corresponding upstream PDL infrastructure. The completeness modules open Lean4GlCoalgebras explicitly when using this interface.