Apply not_TwoRamseyProp_atleast_3_5_13.
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
5,
5,
13 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying atleastp_ref with 3.
The subproof is completed by applying atleastp_ref with 5.