Search for blocks/addresses/...
Proofgold Proof
pf
Apply nat_ordsucc_in_ordsucc with
12
,
9
leaving 2 subgoals.
The subproof is completed by applying nat_12.
The subproof is completed by applying unknownprop_2453a2b3484043c8ce568faca0a1096a3c2d75e863532a7d5d6a9f964c17a76f.
■