Theorem mulRothNumber_lt_of_forall_not_threeGPFree

Modification history