Apply not_TwoRamseyProp_atleast_4_5_24.
Apply TwoRamseyProp_atleastp_atleastp with
4,
4,
5,
5,
24 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying atleastp_ref with 4.
The subproof is completed by applying atleastp_ref with 5.