Apply not_TwoRamseyProp_atleast_3_4_Power_3.
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
10,
4,
prim4 3 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,
4 leaving 2 subgoals.
The subproof is completed by applying nat_10.
The subproof is completed by applying unknownprop_ba23a99d385c96fc20e18f31e2884f35e8c8dc96acf9973b3be03f8c1bfc0b50.