Unbiasing symmetric monoidal categories in Lean. - Robin Carlier (CoRR, 2026)