Apply not_TwoRamseyProp_atleast_4_4_17.
Apply TwoRamseyProp_atleastp_atleastp with
4,
4,
4,
4,
17 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 4.