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