Show the Proof

import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof

	step type	requirements	statement
0	instantiation	1, 2, 3, 4, 5, 6, 7, 8*	, , , , , ,  ⊢
	: , : , :
1	reference	15	⊢
2	theorem		⊢
	proveit.numbers.numerals.decimals.posnat3
3	instantiation	9	⊢
	: , : , :
4	reference	70	⊢
5	reference	69	⊢
6	reference	60	⊢
7	reference	43	⊢
8	instantiation	45, 10, 11	, , , , , ,  ⊢
	: , : , :
9	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
10	instantiation	24, 12	, , , ,  ⊢
	: , : , :
11	instantiation	45, 13, 14	, ,  ⊢
	: , : , :
12	instantiation	15, 16, 17, 70, 69, 60, 18*	, , , ,  ⊢
	: , : , :
13	instantiation	36, 69, 43	,  ⊢
	: , :
14	instantiation	37, 43, 69, 19*	, ,  ⊢
	: , :
15	axiom		⊢
	proveit.numbers.ordering.min_def_multi
16	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
17	instantiation	62	⊢
	: , :
18	instantiation	45, 20, 21	, , , ,  ⊢
	: , : , :
19	instantiation	45, 22, 23	, ,  ⊢
	: , : , :
20	instantiation	24, 25	, ,  ⊢
	: , : , :
21	instantiation	37, 69, 60, 26*	, ,  ⊢
	: , :
22	instantiation	50, 51, 27, 28, 29, 30	, ,  ⊢
	: , : , : , :
23	instantiation	56, 57, 58, 59	⊢
	: , : , : , : , :
24	axiom		⊢
	proveit.logic.equality.substitution
25	instantiation	45, 31, 32	, ,  ⊢
	: , : , :
26	instantiation	45, 33, 34	, ,  ⊢
	: , : , :
27	instantiation	62	⊢
	: , :
28	instantiation	62	⊢
	: , :
29	instantiation	63, 44	⊢
	: , :
30	instantiation	64, 35	, ,  ⊢
	: , :
31	instantiation	36, 70, 69	,  ⊢
	: , :
32	instantiation	37, 69, 70, 38*	, ,  ⊢
	: , :
33	instantiation	50, 51, 39, 40, 41, 42	, ,  ⊢
	: , : , : , :
34	instantiation	56, 57, 58, 59	⊢
	: , : , : , : , :
35	instantiation	68, 43, 69, 44	, ,  ⊢
	: , :
36	theorem		⊢
	proveit.numbers.ordering.min_bin_args_commute
37	axiom		⊢
	proveit.numbers.ordering.min_def_bin
38	instantiation	45, 46, 47	, ,  ⊢
	: , : , :
39	instantiation	62	⊢
	: , :
40	instantiation	62	⊢
	: , :
41	instantiation	63, 61	⊢
	: , :
42	instantiation	64, 48	, ,  ⊢
	: , :
43	assumption		⊢
44	instantiation	66, 49	⊢
	: , :
45	axiom		⊢
	proveit.logic.equality.equals_transitivity
46	instantiation	50, 51, 52, 53, 54, 55	, ,  ⊢
	: , : , : , :
47	instantiation	56, 57, 58, 59	⊢
	: , : , : , : , :
48	instantiation	68, 69, 60, 61	, ,  ⊢
	: , :
49	assumption		⊢
50	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
51	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
52	instantiation	62	⊢
	: , :
53	instantiation	62	⊢
	: , :
54	instantiation	63, 71	⊢
	: , :
55	instantiation	64, 65	, ,  ⊢
	: , :
56	axiom		⊢
	proveit.core_expr_types.conditionals.true_case_reduction
57	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
58	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
59	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
60	assumption		⊢
61	instantiation	66, 67	⊢
	: , :
62	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
63	theorem		⊢
	proveit.core_expr_types.conditionals.satisfied_condition_reduction
64	theorem		⊢
	proveit.core_expr_types.conditionals.dissatisfied_condition_reduction
65	instantiation	68, 69, 70, 71	, ,  ⊢
	: , :
66	theorem		⊢
	proveit.numbers.ordering.relax_less
67	assumption		⊢
68	theorem		⊢
	proveit.numbers.ordering.not_less_from_less_eq
69	assumption		⊢
70	assumption		⊢
71	assumption		⊢
*equality replacement requirements