New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq