Proofgold Proof

pf
Apply nat_trans with u17, u11 leaving 2 subgoals. The subproof is completed by applying nat_17. The subproof is completed by applying unknownprop_fde6379bebd0b99b66d966901300c529916d83c8c1f209841f486bb2568cf012. ■