Combinatorics on Words Formalized