Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: TwoRamseyProp 6 7 (prim4 3).
Apply not_TwoRamseyProp_atleast_3_4_Power_3.
Apply TwoRamseyProp_atleastp_atleastp with 6, 3, 7, 4, prim4 3 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply nat_In_atleastp with 6, 3 leaving 2 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying In_3_6.
Apply nat_In_atleastp with 7, 4 leaving 2 subgoals.
The subproof is completed by applying nat_7.
The subproof is completed by applying In_4_7.