Apply not_TwoRamseyProp_atleast_3_4_Power_3.
Apply TwoRamseyProp_atleastp_atleastp with
4,
3,
9,
4,
prim4 3 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply nat_In_atleastp with
4,
3 leaving 2 subgoals.
The subproof is completed by applying nat_4.
The subproof is completed by applying In_3_4.
Apply nat_In_atleastp with
9,
4 leaving 2 subgoals.
The subproof is completed by applying nat_9.
The subproof is completed by applying In_4_9.