Verified Purely Functional Catenable Real-Time Deques. - Jules Viennot; Arthur Wendling; Armaël Guéneau; François Pottier (CoRR, 2025)