Apply atleastp_tra with prim4 u5, u32, u35 leaving 2 subgoals.

Apply equip_atleastp with prim4 u5, u32.

The subproof is completed by applying unknownprop_4695716882ca379d67a33427761f34c2b061c7b63026aa6ff413df59110ba1a9.

Apply nat_In_atleastp with u35, u32 leaving 2 subgoals.

The subproof is completed by applying unknownprop_a3e012c06fe7317676acef57a26f1aa9ca775c2316f0b3234deabb524335c66f.

Apply ordsuccI1 with ordsucc (ordsucc u32), u32.

Apply ordsuccI1 with ordsucc u32, u32.

The subproof is completed by applying ordsuccI2 with u32.

■

Proofgold Proof