Apply unknownprop_aae4e03000d6619cc34e5a66244db6980d668b70bdfc22610af1046fd13449ea with
3,
6,
24,
prim4 5 leaving 2 subgoals.
Apply atleastp_tra with
24,
32,
prim4 5 leaving 2 subgoals.
Apply nat_In_atleastp with
32,
24 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e20297641bb65d9e51ebac2e053948365a3f53b65d223d41920ce90b2e26b533.
The subproof is completed by applying unknownprop_517d6d8aecf883bffffb5e65645f1bfa2f40dec14b5ac3b5b3dc9b93db3c1ef5.
Apply equip_atleastp with
32,
prim4 5.
Apply equip_sym with
prim4 5,
32.
Apply unknownprop_8e67f22739f9a01fd2d9438edd2f3f6d8d323d1fa4d050bc09f5b1af8d3b6dd7 with
λ x0 x1 . equip (prim4 5) x0.
Apply unknownprop_f5822e9d5891900b4c653eab5e89c5bb71543e61fe2c332750489ecd340604eb with
5.
The subproof is completed by applying nat_5.
The subproof is completed by applying TwoRamseyProp_3_6_24.