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