Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: TwoRamseyProp 4 8 (prim4 4).
Apply not_TwoRamseyProp_atleast_3_6_Power_4.
Apply TwoRamseyProp_atleastp_atleastp with 4, 3, 8, 6, prim4 4 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 8, 6 leaving 2 subgoals.
The subproof is completed by applying nat_8.
The subproof is completed by applying In_6_8.