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	generalization	1	⊢
1	instantiation	11, 2, 3, 9, 4, 5	,  ⊢
	: , : , :
2	instantiation	19, 6	,  ⊢
	: , :
3	instantiation	20, 6	,  ⊢
	: , :
4	deduction	7	,  ⊢
5	deduction	8	,  ⊢
6	instantiation	26, 9	,  ⊢
	:
7	instantiation	53, 10, 51	, ,  ⊢
	: , : , :
8	instantiation	11, 12, 13, 27, 14, 15	, ,  ⊢
	: , : , :
9	instantiation	16, 95, 96	,  ⊢
	: , :
10	instantiation	53, 17, 18	, ,  ⊢
	: , : , :
11	theorem		⊢
	proveit.logic.booleans.disjunction.singular_constructive_dilemma
12	instantiation	19, 21	⊢
	: , :
13	instantiation	20, 21	⊢
	: , :
14	deduction	22	, ,  ⊢
15	deduction	23	, ,  ⊢
16	theorem		⊢
	proveit.numbers.ordering.less_or_greater_eq
17	instantiation	50, 38, 24	, ,  ⊢
	: , : , :
18	instantiation	70, 25, 56	, ,  ⊢
	: , : , :
19	axiom		⊢
	proveit.logic.booleans.disjunction.left_in_bool
20	axiom		⊢
	proveit.logic.booleans.disjunction.right_in_bool
21	instantiation	26, 27	⊢
	:
22	instantiation	53, 28, 38	, , ,  ⊢
	: , : , :
23	instantiation	53, 29, 51	, , ,  ⊢
	: , : , :
24	instantiation	70, 30, 31	, ,  ⊢
	: , : , :
25	instantiation	70, 32, 33	, ,  ⊢
	: , : , :
26	theorem		⊢
	proveit.logic.booleans.in_bool_if_true
27	instantiation	34, 93, 35	⊢
	: , :
28	instantiation	53, 36, 54	, , ,  ⊢
	: , : , :
29	instantiation	53, 37, 38	, , ,  ⊢
	: , : , :
30	instantiation	70, 39, 40	, ,  ⊢
	: , : , :
31	instantiation	73, 75, 74, 76	⊢
	: , : , : , : , :
32	instantiation	82, 41	⊢
	: , : , :
33	instantiation	82, 42	, ,  ⊢
	: , : , :
34	theorem		⊢
	proveit.logic.equality.rhs_via_equality
35	instantiation	43	⊢
	: , :
36	instantiation	98, 44	, ,  ⊢
	: , :
37	instantiation	53, 45, 46	, , ,  ⊢
	: , : , :
38	instantiation	59, 95, 96	,  ⊢
	: , :
39	instantiation	82, 47	, ,  ⊢
	: , : , :
40	instantiation	82, 48	⊢
	: , : , :
41	instantiation	86, 58	⊢
	: , :
42	instantiation	87, 49	, ,  ⊢
	: , :
43	axiom		⊢
	proveit.numbers.ordering.less_eq_def
44	instantiation	50, 51, 52	, ,  ⊢
	: , : , :
45	instantiation	53, 97, 54	, , ,  ⊢
	: , : , :
46	instantiation	70, 55, 56	, ,  ⊢
	: , : , :
47	instantiation	87, 57	, ,  ⊢
	: , :
48	instantiation	86, 67	⊢
	: , :
49	instantiation	92, 95, 96, 58	, ,  ⊢
	: , :
50	theorem		⊢
	proveit.logic.equality.sub_right_side_into
51	instantiation	59, 96, 95	,  ⊢
	: , :
52	instantiation	70, 60, 61	, ,  ⊢
	: , : , :
53	theorem		⊢
	proveit.logic.equality.sub_left_side_into
54	instantiation	70, 62, 63	, ,  ⊢
	: , : , :
55	instantiation	70, 64, 65	, ,  ⊢
	: , : , :
56	instantiation	73, 74, 75, 76	⊢
	: , : , : , : , :
57	instantiation	90, 95, 96, 67	, ,  ⊢
	: , :
58	instantiation	66, 67	⊢
	: , :
59	axiom		⊢
	proveit.numbers.ordering.max_def_bin
60	instantiation	70, 68, 69	, ,  ⊢
	: , : , :
61	instantiation	73, 75, 74, 76	⊢
	: , : , : , : , :
62	instantiation	70, 71, 72	, ,  ⊢
	: , : , :
63	instantiation	73, 74, 75, 76	⊢
	: , : , : , : , :
64	instantiation	82, 77	, ,  ⊢
	: , : , :
65	instantiation	82, 78	, ,  ⊢
	: , : , :
66	theorem		⊢
	proveit.numbers.ordering.relax_less
67	assumption		⊢
68	instantiation	82, 79	, ,  ⊢
	: , : , :
69	instantiation	82, 80	⊢
	: , : , :
70	axiom		⊢
	proveit.logic.equality.equals_transitivity
71	instantiation	82, 81	⊢
	: , : , :
72	instantiation	82, 83	, ,  ⊢
	: , : , :
73	axiom		⊢
	proveit.core_expr_types.conditionals.true_case_reduction
74	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
75	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
76	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
77	instantiation	86, 89	, ,  ⊢
	: , :
78	instantiation	87, 84	, ,  ⊢
	: , :
79	instantiation	87, 85	, ,  ⊢
	: , :
80	instantiation	86, 91	⊢
	: , :
81	instantiation	86, 93	⊢
	: , :
82	axiom		⊢
	proveit.logic.equality.substitution
83	instantiation	87, 88	, ,  ⊢
	: , :
84	instantiation	92, 95, 96, 89	, ,  ⊢
	: , :
85	instantiation	90, 96, 95, 91	, ,  ⊢
	: , :
86	theorem		⊢
	proveit.core_expr_types.conditionals.satisfied_condition_reduction
87	theorem		⊢
	proveit.core_expr_types.conditionals.dissatisfied_condition_reduction
88	instantiation	92, 96, 95, 93	, ,  ⊢
	: , :
89	instantiation	94, 95, 96, 97	, ,  ⊢
	: , :
90	theorem		⊢
	proveit.numbers.ordering.not_less_eq_from_less
91	assumption		⊢
92	theorem		⊢
	proveit.numbers.ordering.not_less_from_less_eq
93	assumption		⊢
94	theorem		⊢
	proveit.numbers.ordering.relax_equal_to_less_eq
95	assumption		⊢
96	assumption		⊢
97	instantiation	98, 99	⊢
	: , :
98	theorem		⊢
	proveit.logic.equality.equals_reversal
99	assumption		⊢