Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: TwoRamseyProp 4 5 24.
Apply not_TwoRamseyProp_atleast_4_5_24.
Apply TwoRamseyProp_atleastp_atleastp with 4, 4, 5, 5, 24 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying atleastp_ref with 4.
The subproof is completed by applying atleastp_ref with 5.