2 ms·

Would have been cool to show it in Coq as well, to make the connection to formal mathematics more clear!