documented some Sledgehammer proof possibilities
documented some Sledgehammer proof possibilities
lemma finite_all_partitions