TY - RPRT TI - Certification of Bilateral Patience Sort in Theorema and Rocq AU - Isabela Drǎmnesc AU - Tudor Jebelean AU - Sorin Stratulat PY - 2026 DO - 10.4204/eptcs.452.10 UR - https://arxiv.org/abs/2609.34889 ID - 2609.34889 ER -