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*	⊢
	: , : , :
1	reference	154	⊢
2	instantiation	342, 338, 8	⊢
	: , : , :
3	instantiation	305, 21, 119, 106	⊢
	: , :
4	instantiation	305, 22, 32, 9	⊢
	: , :
5	instantiation	151, 10, 11	⊢
	: , : , :
6	instantiation	176, 14	⊢
	:
7	instantiation	292, 12, 13	⊢
	: , : , :
8	instantiation	342, 268, 14	⊢
	: , : , :
9	instantiation	15, 16	⊢
	: , :
10	instantiation	17, 35, 18, 134, 19	⊢
	: , : , :
11	instantiation	20, 32, 21, 22, 23, 33	⊢
	: , : , :
12	instantiation	292, 24, 25	⊢
	: , : , :
13	instantiation	26, 27, 28, 29	⊢
	: , : , : , :
14	instantiation	289, 290, 74	⊢
	: , :
15	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
16	instantiation	30, 155, 32, 33	⊢
	: , :
17	theorem		⊢
	proveit.numbers.division.strong_div_from_denom_bound__all_pos
18	instantiation	31, 32, 33	⊢
	:
19	instantiation	34, 134	⊢
	:
20	theorem		⊢
	proveit.numbers.division.weak_div_from_numer_bound__pos_denom
21	instantiation	342, 258, 35	⊢
	: , : , :
22	instantiation	36, 37	⊢
	:
23	instantiation	38, 39, 40, 41*	⊢
	:
24	instantiation	233, 42	⊢
	: , : , :
25	instantiation	190, 43, 44	⊢
	: , : , :
26	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
27	instantiation	233, 45	⊢
	: , : , :
28	instantiation	233, 46	⊢
	: , : , :
29	instantiation	112, 47, 113, 328	⊢
	: , : , :
30	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq
31	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
32	instantiation	48, 155, 306, 50	⊢
	: , : , :
33	instantiation	49, 155, 306, 50	⊢
	: , : , :
34	theorem		⊢
	proveit.trigonometry.sine_linear_bound_by_arg_pos
35	instantiation	51, 144, 145, 52, 53, 259	⊢
	: , :
36	theorem		⊢
	proveit.trigonometry.real_closure
37	instantiation	190, 54, 55	⊢
	: , : , :
38	theorem		⊢
	proveit.trigonometry.sine_linear_bound_nonneg
39	instantiation	56, 144, 97, 57, 58, 59	⊢
	: , :
40	instantiation	167, 60, 61	⊢
	: , : , :
41	instantiation	292, 62, 63	⊢
	: , : , :
42	instantiation	292, 64, 65	⊢
	: , : , :
43	instantiation	190, 66, 67	⊢
	: , : , :
44	instantiation	292, 68, 69	⊢
	: , : , :
45	instantiation	196, 328, 209	⊢
	: , :
46	instantiation	196, 208, 209	⊢
	: , :
47	instantiation	342, 140, 70	⊢
	: , : , :
48	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
49	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
50	instantiation	71, 72	⊢
	:
51	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure
52	instantiation	342, 73, 291	⊢
	: , : , :
53	instantiation	342, 73, 74	⊢
	: , : , :
54	instantiation	219, 75, 232	⊢
	: , :
55	instantiation	194, 250, 344, 337, 251, 76, 255, 208, 209	⊢
	: , : , : , : , : , :
56	theorem		⊢
	proveit.numbers.multiplication.mult_real_nonneg_closure
57	instantiation	342, 77, 78	⊢
	: , : , :
58	instantiation	342, 79, 257	⊢
	: , : , :
59	instantiation	342, 79, 259	⊢
	: , : , :
60	instantiation	167, 153, 80	⊢
	: , : , :
61	instantiation	81, 208, 328, 307, 82*	⊢
	: , :
62	instantiation	233, 83	⊢
	: , : , :
63	instantiation	292, 84, 85	⊢
	: , : , :
64	instantiation	142, 250, 337, 251, 328, 255, 209	⊢
	: , : , : , : , : , : , :
65	instantiation	143, 337, 344, 250, 86, 251, 255, 328, 209	⊢
	: , : , : , : , : , :
66	instantiation	87, 261, 104, 114, 88, 89	⊢
	: , : , : , : , :
67	instantiation	233, 90	⊢
	: , : , :
68	instantiation	233, 91	⊢
	: , : , :
69	instantiation	326, 92	⊢
	:
70	instantiation	342, 146, 259	⊢
	: , : , :
71	theorem		⊢
	proveit.trigonometry.sine_pos_interval
72	instantiation	93, 155, 231, 119, 94	⊢
	: , : , :
73	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
74	instantiation	342, 309, 317	⊢
	: , : , :
75	instantiation	219, 282, 231	⊢
	: , :
76	instantiation	325	⊢
	: , :
77	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
78	instantiation	342, 95, 298	⊢
	: , : , :
79	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonneg
80	instantiation	142, 250, 337, 251, 255, 208, 209	⊢
	: , : , : , : , : , : , :
81	theorem		⊢
	proveit.numbers.division.div_as_mult
82	instantiation	292, 96, 175	⊢
	: , : , :
83	instantiation	194, 337, 144, 250, 97, 251, 328, 255, 208, 209	⊢
	: , : , : , : , : , :
84	instantiation	292, 98, 99	⊢
	: , : , :
85	instantiation	102, 115	⊢
	:
86	instantiation	325	⊢
	: , :
87	theorem		⊢
	proveit.numbers.division.mult_frac_cancel_denom_left
88	instantiation	342, 140, 100	⊢
	: , : , :
89	instantiation	342, 140, 121	⊢
	: , : , :
90	instantiation	233, 101	⊢
	: , : , :
91	instantiation	102, 261	⊢
	:
92	instantiation	103, 104, 105, 106	⊢
	: , :
93	theorem		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalOO
94	instantiation	107, 108, 109	⊢
	: , :
95	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
96	instantiation	233, 110	⊢
	: , : , :
97	instantiation	164	⊢
	: , : , :
98	instantiation	233, 111	⊢
	: , : , :
99	instantiation	112, 113, 114, 115, 116*	⊢
	: , : , :
100	instantiation	342, 162, 117	⊢
	: , : , :
101	instantiation	326, 255	⊢
	:
102	theorem		⊢
	proveit.numbers.division.frac_one_denom
103	theorem		⊢
	proveit.numbers.division.div_complex_closure
104	instantiation	118, 328, 209	⊢
	: , :
105	instantiation	342, 334, 119	⊢
	: , : , :
106	instantiation	120, 121	⊢
	:
107	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
108	instantiation	218, 134	⊢
	:
109	instantiation	122, 123, 124	⊢
	: , : , :
110	instantiation	125, 126, 308, 248*	⊢
	: , :
111	instantiation	292, 127, 128	⊢
	: , : , :
112	theorem		⊢
	proveit.numbers.division.frac_cancel_left
113	instantiation	342, 140, 129	⊢
	: , : , :
114	instantiation	342, 140, 130	⊢
	: , : , :
115	instantiation	190, 131, 132	⊢
	: , : , :
116	instantiation	327, 208	⊢
	:
117	instantiation	342, 184, 133	⊢
	: , : , :
118	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
119	instantiation	342, 258, 134	⊢
	: , : , :
120	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
121	instantiation	342, 146, 134	⊢
	: , : , :
122	axiom		⊢
	proveit.numbers.ordering.transitivity_less_less
123	instantiation	190, 135, 169	⊢
	: , : , :
124	instantiation	202, 199, 136, 137, 138*, 139*	⊢
	: , : , :
125	theorem		⊢
	proveit.numbers.exponentiation.neg_power_as_div
126	instantiation	342, 140, 141	⊢
	: , : , :
127	instantiation	142, 250, 344, 337, 251, 149, 328, 255, 208, 209	⊢
	: , : , : , : , : , : , :
128	instantiation	143, 337, 144, 250, 145, 251, 208, 328, 255, 209	⊢
	: , : , : , : , : , :
129	instantiation	342, 146, 257	⊢
	: , : , :
130	instantiation	342, 162, 147	⊢
	: , : , :
131	instantiation	342, 334, 148	⊢
	: , : , :
132	instantiation	194, 250, 344, 337, 251, 149, 328, 255, 209	⊢
	: , : , : , : , : , :
133	instantiation	342, 201, 317	⊢
	: , : , :
134	instantiation	150, 257, 259	⊢
	: , :
135	instantiation	151, 152, 153	⊢
	: , : , :
136	instantiation	219, 220, 155	⊢
	: , :
137	instantiation	154, 220, 155, 231, 193, 156	⊢
	: , : , :
138	instantiation	292, 157, 158	⊢
	: , : , :
139	instantiation	159, 160, 161*	⊢
	: , :
140	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
141	instantiation	342, 162, 163	⊢
	: , : , :
142	theorem		⊢
	proveit.numbers.multiplication.leftward_commutation
143	theorem		⊢
	proveit.numbers.multiplication.association
144	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
145	instantiation	164	⊢
	: , : , :
146	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
147	instantiation	342, 184, 165	⊢
	: , : , :
148	instantiation	219, 166, 232	⊢
	: , :
149	instantiation	325	⊢
	: , :
150	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
151	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
152	instantiation	167, 168, 169	⊢
	: , : , :
153	instantiation	170, 231, 171, 287, 172, 173, 174*, 175*	⊢
	: , : , :
154	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
155	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
156	instantiation	176, 269	⊢
	:
157	instantiation	233, 177	⊢
	: , : , :
158	instantiation	178, 179	⊢
	:
159	theorem		⊢
	proveit.logic.equality.equals_reversal
160	instantiation	180, 250, 344, 337, 251, 181, 198, 208	⊢
	: , : , : , : , : , :
161	instantiation	292, 182, 183	⊢
	: , : , :
162	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
163	instantiation	342, 184, 185	⊢
	: , : , :
164	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
165	instantiation	342, 201, 308	⊢
	: , : , :
166	instantiation	219, 335, 282	⊢
	: , :
167	theorem		⊢
	proveit.logic.equality.sub_left_side_into
168	instantiation	186, 337, 257, 259, 187, 188*	⊢
	: , : , : , : , : , :
169	instantiation	233, 189	⊢
	: , : , :
170	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
171	instantiation	219, 282, 232	⊢
	: , :
172	instantiation	190, 191, 192	⊢
	: , : , :
173	instantiation	266, 193	⊢
	: , :
174	instantiation	194, 337, 344, 250, 195, 251, 208, 255, 209	⊢
	: , : , : , : , : , :
175	instantiation	196, 208, 198	⊢
	: , :
176	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
177	instantiation	197, 198	⊢
	:
178	theorem		⊢
	proveit.numbers.addition.elim_zero_left
179	instantiation	342, 334, 199	⊢
	: , : , :
180	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
181	instantiation	325	⊢
	: , :
182	instantiation	233, 200	⊢
	: , : , :
183	instantiation	326, 208	⊢
	:
184	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
185	instantiation	342, 201, 324	⊢
	: , : , :
186	theorem		⊢
	proveit.numbers.multiplication.strong_bound_via_factor_bound
187	instantiation	202, 281, 335, 203, 204, 205*, 206*	⊢
	: , : , :
188	instantiation	207, 337, 208, 209	⊢
	: , : , : , :
189	instantiation	292, 210, 211	⊢
	: , : , :
190	theorem		⊢
	proveit.logic.equality.sub_right_side_into
191	instantiation	212, 213, 214	⊢
	: , :
192	instantiation	215, 324, 216, 255, 303, 217*	⊢
	: , :
193	instantiation	218, 257	⊢
	:
194	theorem		⊢
	proveit.numbers.multiplication.disassociation
195	instantiation	325	⊢
	: , :
196	theorem		⊢
	proveit.numbers.multiplication.commutation
197	theorem		⊢
	proveit.numbers.multiplication.mult_zero_right
198	instantiation	342, 334, 287	⊢
	: , : , :
199	instantiation	219, 220, 231	⊢
	: , :
200	instantiation	221, 333, 341, 222*	⊢
	: , : , : , :
201	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
202	theorem		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
203	instantiation	342, 338, 223	⊢
	: , : , :
204	instantiation	224, 335, 282, 306, 225, 226	⊢
	: , : , :
205	instantiation	227, 261, 328, 228	⊢
	: , : , :
206	instantiation	292, 229, 230	⊢
	: , : , :
207	theorem		⊢
	proveit.numbers.multiplication.elim_one_any
208	instantiation	342, 334, 231	⊢
	: , : , :
209	instantiation	342, 334, 232	⊢
	: , : , :
210	instantiation	233, 234	⊢
	: , : , :
211	instantiation	235, 303	⊢
	:
212	theorem		⊢
	proveit.numbers.absolute_value.weak_upper_bound
213	instantiation	236, 264, 287, 265	⊢
	: , : , :
214	instantiation	266, 237	⊢
	: , :
215	theorem		⊢
	proveit.numbers.absolute_value.abs_prod
216	instantiation	325	⊢
	: , :
217	instantiation	238, 239	⊢
	:
218	theorem		⊢
	proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos
219	theorem		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
220	instantiation	342, 338, 240	⊢
	: , : , :
221	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
222	instantiation	292, 241, 242	⊢
	: , : , :
223	instantiation	342, 340, 243	⊢
	: , : , :
224	theorem		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
225	instantiation	244, 335, 306, 245, 246, 247, 248*	⊢
	: , : , :
226	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
227	theorem		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
228	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
229	instantiation	249, 250, 344, 337, 251, 252, 255, 261, 253	⊢
	: , : , : , : , : , :
230	instantiation	254, 261, 255, 256	⊢
	: , : , :
231	instantiation	342, 258, 257	⊢
	: , : , :
232	instantiation	342, 258, 259	⊢
	: , : , :
233	axiom		⊢
	proveit.logic.equality.substitution
234	instantiation	260, 261, 303, 262*	⊢
	: , :
235	theorem		⊢
	proveit.numbers.absolute_value.abs_even
236	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
237	instantiation	263, 264, 287, 265	⊢
	: , : , :
238	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
239	instantiation	266, 267	⊢
	: , :
240	instantiation	342, 268, 269	⊢
	: , : , :
241	instantiation	310, 344, 270, 271, 272, 273	⊢
	: , : , : , :
242	instantiation	274, 275, 276	⊢
	:
243	instantiation	342, 343, 277	⊢
	: , : , :
244	theorem		⊢
	proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
245	instantiation	300, 301, 279	⊢
	: , : , :
246	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
247	instantiation	278, 279	⊢
	:
248	instantiation	280, 328	⊢
	:
249	theorem		⊢
	proveit.numbers.addition.disassociation
250	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
251	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
252	instantiation	325	⊢
	: , :
253	instantiation	342, 334, 281	⊢
	: , : , :
254	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
255	instantiation	342, 334, 282	⊢
	: , : , :
256	instantiation	283	⊢
	:
257	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pi_is_real_pos
258	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
259	instantiation	284, 285	⊢
	:
260	theorem		⊢
	proveit.numbers.multiplication.mult_neg_left
261	instantiation	342, 334, 306	⊢
	: , : , :
262	instantiation	326, 303	⊢
	:
263	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
264	instantiation	286, 287	⊢
	:
265	theorem		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_round_in_interval
266	theorem		⊢
	proveit.numbers.ordering.relax_less
267	instantiation	288, 317	⊢
	:
268	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
269	instantiation	289, 290, 291	⊢
	: , :
270	instantiation	325	⊢
	: , :
271	instantiation	325	⊢
	: , :
272	instantiation	292, 293, 294	⊢
	: , : , :
273	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
274	theorem		⊢
	proveit.numbers.division.frac_cancel_complete
275	instantiation	342, 334, 295	⊢
	: , : , :
276	instantiation	323, 296	⊢
	:
277	instantiation	297, 298, 337	⊢
	: , :
278	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
279	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
280	theorem		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
281	instantiation	342, 338, 299	⊢
	: , : , :
282	instantiation	300, 301, 317	⊢
	: , : , :
283	axiom		⊢
	proveit.logic.equality.equals_reflexivity
284	theorem		⊢
	proveit.numbers.absolute_value.abs_nonzero_closure
285	instantiation	302, 303, 304	⊢
	:
286	theorem		⊢
	proveit.numbers.negation.real_closure
287	instantiation	305, 306, 335, 307	⊢
	: , :
288	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
289	theorem		⊢
	proveit.numbers.division.div_rational_pos_closure
290	instantiation	342, 309, 308	⊢
	: , : , :
291	instantiation	342, 309, 324	⊢
	: , : , :
292	axiom		⊢
	proveit.logic.equality.equals_transitivity
293	instantiation	310, 344, 311, 312, 313, 314	⊢
	: , : , : , :
294	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_2
295	instantiation	342, 338, 315	⊢
	: , : , :
296	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
297	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
298	instantiation	342, 316, 317	⊢
	: , : , :
299	instantiation	342, 340, 318	⊢
	: , : , :
300	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
301	instantiation	319, 320	⊢
	: , :
302	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero
303	instantiation	342, 334, 321	⊢
	: , : , :
304	assumption		⊢
305	theorem		⊢
	proveit.numbers.division.div_real_closure
306	instantiation	342, 338, 322	⊢
	: , : , :
307	instantiation	323, 324	⊢
	:
308	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
309	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
310	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
311	instantiation	325	⊢
	: , :
312	instantiation	325	⊢
	: , :
313	instantiation	326, 328	⊢
	:
314	instantiation	327, 328	⊢
	:
315	instantiation	342, 340, 329	⊢
	: , : , :
316	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
317	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
318	instantiation	330, 333	⊢
	:
319	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
320	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
321	instantiation	331, 332	⊢
	:
322	instantiation	342, 340, 333	⊢
	: , : , :
323	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
324	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
325	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
326	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
327	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
328	instantiation	342, 334, 335	⊢
	: , : , :
329	instantiation	342, 343, 336	⊢
	: , : , :
330	theorem		⊢
	proveit.numbers.negation.int_closure
331	theorem		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
332	theorem		⊢
	proveit.physics.quantum.QPE._best_round_is_int
333	instantiation	342, 343, 337	⊢
	: , : , :
334	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
335	instantiation	342, 338, 339	⊢
	: , : , :
336	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
337	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
338	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
339	instantiation	342, 340, 341	⊢
	: , : , :
340	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
341	instantiation	342, 343, 344	⊢
	: , : , :
342	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
343	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
344	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements