Search for blocks/addresses/...
Proofgold Proof
pf
Apply nat_ordsucc_in_ordsucc with
10
,
1
leaving 2 subgoals.
The subproof is completed by applying nat_10.
The subproof is completed by applying unknownprop_1b6aea42dd8dd6467e5f0150bab2b0d6533055acdd61b232a0adb5a2a42e1655.
■