Apply not_TwoRamseyProp_atleast_3_6_Power_4.
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
10,
6,
prim4 4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying atleastp_ref with 3.
Apply nat_In_atleastp with
10,
6 leaving 2 subgoals.
The subproof is completed by applying nat_10.
The subproof is completed by applying unknownprop_fd78d9827713c0f7b71247ad97a24b91bc3ec9128c1ed685c74b49de36aa650c.