Search for blocks/addresses/...
Proofgold Proof
pf
Apply nat_ordsucc_in_ordsucc with
13
,
11
leaving 2 subgoals.
The subproof is completed by applying nat_13.
The subproof is completed by applying unknownprop_d0b907f11f7106146d29548fcb3a49e74411d92136323f4b4174f28479e56fcb.
■