2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
12 include "arithmetics/log.ma".
13 include "arithmetics/sigma_pi.ma".
14 include "arithmetics/ord.ma".
16 (* (prim n) counts the number of prime numbers up to n included *)
17 definition prim ≝ λn. ∑_{i < S n | primeb i} 1.
19 lemma le_prim_n: ∀n. prim n ≤ n.
21 whd in ⊢ (?%?); cases (primeb (S n)) whd in ⊢ (?%?);
22 [@le_S_S @H |@le_S @H]
25 lemma not_prime_times_2: ∀n. 1 < n → ¬prime (2*n).
26 #n #ltn % * #H #H1 @(absurd (2 = 2*n))
28 |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r //
32 theorem eq_prim_prim_pred: ∀n. 1 < n →
33 prim (2*n) = prim (pred (2*n)).
35 lapply (S_pred (2*n) ?) [>(times_n_1 0) in ⊢ (?%?); @lt_times //] #H2n
36 lapply (not_prime_times_2 n ltn) #notp2n
37 whd in ⊢ (??%?); >(not_prime_to_primeb_false … notp2n) whd in ⊢ (??%?);
41 theorem le_prim_n1: ∀n. 4 ≤ n →
45 |#m #le4 cut (S (2*m) = pred (2*(S m))) [normalize //] #Heq >Heq
46 <eq_prim_prim_pred [2: @le_S_S @(transitive_le … le4) //]
47 #H whd in ⊢ (?%?); cases (primeb (S (2*S m)))
48 [@le_S_S @H |@le_S @H]
52 (* usefull to kill a successor in bertrand *)
53 theorem le_prim_n2: ∀n. 7 ≤ n → prim (S(2*n)) ≤ pred n.
56 |#m #le7 cut (S (2*m) = pred (2*(S m))) [normalize //] #Heq >Heq
57 <eq_prim_prim_pred [2: @le_S_S @(transitive_le … le7) //]
59 whd in ⊢ (??%); <(S_pred m) in ⊢ (??%); [2: @(transitive_le … le7) //]
60 cases (primeb (S (2*S m))) [@le_S_S @H |@le_S @H]
64 lemma even_or_odd: ∀n.∃a.n=2*a ∨ n = S(2*a).
67 |#n * #a * #Hn [%{a} %2 @eq_f @Hn | %{(S a)} %1 >Hn normalize //
71 (* la prova potrebbe essere migliorata *)
72 theorem le_prim_n3: ∀n. 15 ≤ n →
74 #n #len cases (even_or_odd (pred n)) #a * #Hpredn
75 [cut (n = S (2*a)) [<Hpredn @sym_eq @S_pred @(transitive_le … len) //] #Hn
76 >Hn @(transitive_le ? (pred a))
77 [@le_prim_n2 @(le_times_to_le 2) [//|@le_S_S_to_le <Hn @len]
78 |@monotonic_pred @le_times_to_le_div //
81 [normalize normalize in Hpredn:(???%); <plus_n_Sm <Hpredn @sym_eq @S_pred
82 @(transitive_le … len) //] #Hn
83 >Hn @(transitive_le ? (pred a))
85 [2:@(lt_times_n_to_lt_r 2) <Hn @(transitive_le … len) //]
86 <Hn >Hpredn @le_prim_n2 @le_S_S_to_le @(lt_times_n_to_lt_r 2) <Hn @len
87 |@monotonic_pred @le_times_to_le_div //
92 (* This is chebishev psi function *)
93 definition A: nat → nat ≝
94 λn.∏_{p < S n | primeb p} (exp p (log p n)).
96 definition psi_def : ∀n.
97 A n = ∏_{p < S n | primeb p} (exp p (log p n)).
101 A n ≤ ∏_{p < S n | primeb p} n.
102 #n cases n [@le_n |#m @le_pi #i #_ #_ @le_exp_log //]
105 theorem le_Al: ∀n. A n ≤ exp n (prim n).
106 #n <exp_sigma @le_Al1
110 exp n (prim n) ≤ A n * A n.
111 #n elim (le_to_or_lt_eq ?? (le_O_n n)) #Hn
112 [<(exp_sigma (S n) n primeb) <times_pi
113 @le_pi #i #lti #primei
115 [@(lt_to_le_to_lt … (le_S_S_to_le … lti)) @prime_to_lt_SO
116 @primeb_true_to_prime //] #lt1n
118 @(transitive_le ? (exp i (S(log i n))))
119 [@lt_to_le @lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
121 [@prime_to_lt_O @primeb_true_to_prime //
122 |>(plus_n_O (log i n)) in ⊢ (?%?); >plus_n_Sm
123 @monotonic_le_plus_r @lt_O_log //
131 (* an equivalent formulation for psi *)
132 definition A': nat → nat ≝
133 λn. ∏_{p < S n | primeb p} (∏_{i < log p n} p).
135 lemma Adef: ∀n. A' n = ∏_{p < S n | primeb p} (∏_{i < log p n} p).
138 theorem eq_A_A': ∀n.A n = A' n.
139 #n @same_bigop // #i #lti #primebi
140 @(trans_eq ? ? (exp i (∑_{x < log i n} 1)))
141 [@eq_f @sym_eq @sigma_const
146 theorem eq_pi_p_primeb_divides_b: ∀n,m.
147 ∏_{p<n | primeb p ∧ dividesb p m} (exp p (ord m p))
148 = ∏_{p<n | primeb p} (exp p (ord m p)).
149 #n #m elim n // #n1 #Hind cases (true_or_false (primeb n1)) #Hprime
150 [>bigop_Strue in ⊢ (???%); //
151 cases (true_or_false (dividesb n1 m)) #Hdivides
152 [>bigop_Strue [@eq_f @Hind| @true_to_andb_true //]
154 [>not_divides_to_ord_O
155 [whd in ⊢ (???(?%?)); //
156 |@dividesb_false_to_not_divides //
157 |@primeb_true_to_prime //
162 |>bigop_Sfalse [>bigop_Sfalse // |>Hprime %]
166 (* integrations to minimization *)
167 theorem false_to_lt_max: ∀f,n,m.O < n →
168 f n = false → max m f ≤ n → max m f < n.
169 #f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax
171 |cases (exists_max_forall_false f m)
172 [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) //
178 (* integrations to minimization *)
179 lemma lt_1_max_prime: ∀n. 1 < n →
180 1 < max (S n) (λi:nat.primeb i∧dividesb i n).
182 @(lt_to_le_to_lt ? (smallest_factor n))
183 [@lt_SO_smallest_factor //
185 [@le_S_S @le_smallest_factor_n
187 [@prime_to_primeb_true @prime_smallest_factor_n //
188 |@divides_to_dividesb_true
189 [@lt_O_smallest_factor @lt_to_le //
190 |@divides_smallest_factor_n @lt_to_le //
197 theorem lt_max_to_pi_p_primeb: ∀q,m. O<m → max (S m) (λi.primeb i ∧ dividesb i m)<q →
198 m = ∏_{p < q | primeb p ∧ dividesb p m} (exp p (ord m p)).
200 [#m #posm #Hmax normalize @False_ind @(absurd … Hmax (not_le_Sn_O ?))
201 |#n #Hind #m #posm #Hmax
202 cases (true_or_false (primeb n∧dividesb n m)) #Hcase
204 [>(exp_ord n m … posm) in ⊢ (??%?);
205 [@eq_f >(Hind (ord_rem m n))
207 [#x #ltxn cases (true_or_false (primeb x)) #Hx >Hx
208 [cases (true_or_false (dividesb x (ord_rem m n))) #Hx1 >Hx1
209 [@sym_eq @divides_to_dividesb_true
210 [@prime_to_lt_O @primeb_true_to_prime //
211 |@(transitive_divides ? (ord_rem m n))
212 [@dividesb_true_to_divides //
213 |@(divides_ord_rem … posm) @(transitive_lt … ltxn)
214 @prime_to_lt_SO @primeb_true_to_prime //
217 |@sym_eq @not_divides_to_dividesb_false
218 [@prime_to_lt_O @primeb_true_to_prime //
219 |@(ord_O_to_not_divides … posm)
220 [@primeb_true_to_prime //
221 |<(ord_ord_rem n … posm … ltxn)
222 [@not_divides_to_ord_O
223 [@primeb_true_to_prime //
224 |@dividesb_false_to_not_divides //
226 |@primeb_true_to_prime //
227 |@primeb_true_to_prime @(andb_true_l ?? Hcase)
234 |#x #ltxn #Hx @eq_f @ord_ord_rem //
235 [@primeb_true_to_prime @(andb_true_l ? ? Hcase)
236 |@primeb_true_to_prime @(andb_true_l ? ? Hx)
240 [elim (exists_max_forall_false (λi:nat.primeb i∧dividesb i (ord_rem m n)) (S(ord_rem m n)))
241 [* #Hex #Hord_rem cases Hex #x * #H6 #H7 % #H
242 >H in Hord_rem; #Hn @(absurd ?? (not_divides_ord_rem m n posm ?))
243 [@dividesb_true_to_divides @(andb_true_r ?? Hn)
244 |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hn)
246 |* #Hall #Hmax >Hmax @lt_to_not_eq @prime_to_lt_O
247 @primeb_true_to_prime @(andb_true_l ?? Hcase)
249 |@(transitive_le ? (max (S m) (λi:nat.primeb i∧dividesb i (ord_rem m n))))
250 [@le_to_le_max @le_S_S @(divides_to_le … posm) @(divides_ord_rem … posm)
251 @prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase)
252 |@(transitive_le ? (max (S m) (λi:nat.primeb i∧dividesb i m)))
253 [@le_max_f_max_g #i #ltim #Hi
254 cases (true_or_false (primeb i)) #Hprimei >Hprimei
255 [@divides_to_dividesb_true
256 [@prime_to_lt_O @primeb_true_to_prime //
257 |@(transitive_divides ? (ord_rem m n))
258 [@dividesb_true_to_divides @(andb_true_r ?? Hi)
259 |@(divides_ord_rem … posm)
260 @prime_to_lt_SO @primeb_true_to_prime
261 @(andb_true_l ?? Hcase)
264 |>Hprimei in Hi; #Hi @Hi
270 |@(lt_O_ord_rem … posm) @prime_to_lt_SO
271 @primeb_true_to_prime @(andb_true_l ?? Hcase)
273 |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase)
277 |cases (le_to_or_lt_eq ?? posm) #Hm
279 [@(Hind … posm) @false_to_lt_max
280 [@(lt_to_le_to_lt ? (max (S m) (λi:nat.primeb i∧dividesb i m)))
281 [@lt_to_le @lt_1_max_prime //
290 <(bigop_false (S n) ? 1 times (λp:nat.p\sup(ord 1 p))) in ⊢ (??%?);
292 [#i #lein cases (true_or_false (primeb i)) #primei >primei //
293 @sym_eq @not_divides_to_dividesb_false
294 [@prime_to_lt_O @primeb_true_to_prime //
295 |% #divi @(absurd ?? (le_to_not_lt i 1 ?))
296 [@prime_to_lt_SO @(primeb_true_to_prime ? primei)
307 (* factorization of n into primes *)
308 theorem pi_p_primeb_dividesb: ∀n. O < n →
309 n = ∏_{ p < S n | primeb p ∧ dividesb p n} (exp p (ord n p)).
310 #n #posn @lt_max_to_pi_p_primeb // @lt_max_n @le_S @posn
313 theorem pi_p_primeb: ∀n. O < n →
314 n = ∏_{ p < (S n) | primeb p}(exp p (ord n p)).
315 #n #posn <eq_pi_p_primeb_divides_b @pi_p_primeb_dividesb //
318 theorem le_ord_log: ∀n,p. O < n → 1 < p →
320 #n #p #posn #lt1p >(exp_ord p ? lt1p posn) in ⊢ (??(??%));
321 >log_exp // @lt_O_ord_rem //
324 theorem sigma_p_dividesb:
325 ∀m,n,p. O < n → prime p → p ∤ n →
326 m = ∑_{ i < m | dividesb (p\sup (S i)) ((exp p m)*n)} 1.
327 #m elim m // -m #m #Hind #n #p #posn #primep #ndivp
329 [>commutative_plus <plus_n_Sm @eq_f <plus_n_O
330 >(Hind n p posn primep ndivp) in ⊢ (? ? % ?);
332 [#i #ltim cases (true_or_false (dividesb (p\sup(S i)) (p\sup m*n))) #Hc >Hc
333 [@sym_eq @divides_to_dividesb_true
334 [@lt_O_exp @prime_to_lt_O //
335 |%{((exp p (m - i))*n)} <associative_times
336 <exp_plus_times @eq_f2 // @eq_f normalize @eq_f >commutative_plus
337 @plus_minus_m_m @lt_to_le //
339 |@False_ind @(absurd ?? (dividesb_false_to_not_divides ? ? Hc))
340 %{((exp p (m - S i))*n)} <associative_times <exp_plus_times @eq_f2
341 [@eq_f >commutative_plus @plus_minus_m_m //
348 |@divides_to_dividesb_true
349 [@lt_O_exp @prime_to_lt_O // | %{n} //]
353 theorem sigma_p_dividesb1:
354 ∀m,n,p,k. O < n → prime p → p ∤ n → m ≤ k →
355 m = ∑_{i < k | dividesb (p\sup (S i)) ((exp p m)*n)} 1.
356 #m #n #p #k #posn #primep #ndivp #lemk
357 lapply (prime_to_lt_SO ? primep) #lt1p
358 lapply (prime_to_lt_O ? primep) #posp
359 >(sigma_p_dividesb m n p posn primep ndivp) in ⊢ (??%?);
360 >(pad_bigop k m) // @same_bigop
361 [#i #ltik cases (true_or_false (leb m i)) #Him > Him
362 [whd in ⊢(??%?); @sym_eq
363 @not_divides_to_dividesb_false
365 |lapply (leb_true_to_le … Him) -Him #Him
366 % #Hdiv @(absurd ?? (le_to_not_lt ?? Him))
367 (* <(ord_exp p m lt1p) *) >(plus_n_O m)
368 <(not_divides_to_ord_O ?? primep ndivp)
371 [whd <(ord_exp p (S i) lt1p)
372 @divides_to_le_ord //
374 |>(times_n_O O) @lt_times // @lt_O_exp //
385 theorem eq_ord_sigma_p:
386 ∀n,m,x. O < n → prime x →
387 exp x m ≤ n → n < exp x (S m) →
388 ord n x= ∑_{i < m | dividesb (x\sup (S i)) n} 1.
389 #n #m #x #posn #primex #Hexp #ltn
390 lapply (prime_to_lt_SO ? primex) #lt1x
391 >(exp_ord x n) in ⊢ (???%); // @sigma_p_dividesb1
394 |@not_divides_ord_rem //
395 |@le_S_S_to_le @(le_to_lt_to_lt ? (log x n))
399 |@(le_to_lt_to_lt ? n ? ? ltn) @le_exp_log //
405 theorem pi_p_primeb1: ∀n. O < n →
406 n = ∏_{p < S n| primeb p}
407 (∏_{i < log p n| dividesb (exp p (S i)) n} p).
408 #n #posn >(pi_p_primeb n posn) in ⊢ (??%?);
411 |#p #ltp #primep >exp_sigma @eq_f @eq_ord_sigma_p
413 |@primeb_true_to_prime //
415 |@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
420 (* the factorial function *)
421 theorem eq_fact_pi_p:∀n.
422 fact n = ∏_{i < S n | leb 1 i} i.
423 #n elim n // #n1 #Hind whd in ⊢ (??%?); >commutative_times >bigop_Strue
427 theorem eq_sigma_p_div: ∀n,q.O < q →
428 ∑_{ m < S n | leb (S O) m ∧ dividesb q m} 1 =n/q.
430 @(div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
434 [normalize cases q //
435 |#n1 #Hind cases (or_div_mod1 n1 q posq)
436 [* #divq #eqn1 >divides_to_mod_O //
437 <plus_n_O >bigop_Strue
438 [>eqn1 in ⊢ (??%?); @eq_f2
439 [<commutative_plus <plus_n_Sm <plus_n_O @eq_f
440 @(div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
441 [@div_mod_spec_div_mod //
442 |@div_mod_spec_intro [@lt_mod_m_m // | //]
446 |@true_to_andb_true [//|@divides_to_dividesb_true //]
448 |* #ndiv #eqn1 >bigop_Sfalse
450 [< plus_n_Sm @eq_f //
451 |cases (le_to_or_lt_eq (S (mod n1 q)) q ?)
453 |#eqq @False_ind cases ndiv #Hdiv @Hdiv
454 %{(S(div n1 q))} <times_n_Sm <commutative_plus //
458 |>not_divides_to_dividesb_false //
463 |@div_mod_spec_div_mod //
467 lemma timesACdef: ∀n,m. timesAC n m = n * m.
470 (* still another characterization of the factorial *)
471 theorem fact_pi_p: ∀n.
472 fact n = ∏_{ p < S n | primeb p}
473 (∏_{i < log p n} (exp p (n /(exp p (S i))))).
476 (∏_{m < S n | leb 1 m}
477 (∏_{p < S m | primeb p}
478 (∏_{i < log p m | dividesb (exp p (S i)) m} p))))
479 [@same_bigop [// |#x #Hx1 #Hx2 @pi_p_primeb1 @leb_true_to_le //]
481 (∏_{m < S n | leb 1 m}
482 (∏_{p < S m | primeb p ∧ leb p m}
483 (∏_{ i < log p m | dividesb ((p)\sup(S i)) m} p))))
486 |#x #Hx1 #Hx2 @same_bigop
487 [#p #ltp >(le_to_leb_true … (le_S_S_to_le …ltp))
493 (∏_{m < S n | leb 1 m}
494 (∏_{p < S n | primeb p ∧ leb p m}
495 (∏_{i < log p m |dividesb ((p)\sup(S i)) m} p))))
498 |#p #Hp1 #Hp2 @pad_bigop1
500 |#i #lti #upi >lt_to_leb_false
501 [cases (primeb i) //|@lti]
504 |(* make a general theorem *)
506 (∏_{p < S n | primeb p}
507 (∏_{m < S n | leb p m}
508 (∏_{i < log p m | dividesb (p^(S i)) m} p))))
509 [@(bigop_commute … timesAC … (lt_O_S n) (lt_O_S n))
511 cases (true_or_false (primeb j ∧ leb j i)) #Hc >Hc
512 [>(le_to_leb_true 1 i)
514 |@(transitive_le ? j)
515 [@prime_to_lt_O @primeb_true_to_prime @(andb_true_l ? ? Hc)
516 |@leb_true_to_le @(andb_true_r ?? Hc)
525 (∏_{m < S n | leb p m}
526 (∏_{i < log p n | dividesb (p\sup(S i)) m} p)))
529 |#x #Hx1 #Hx2 @sym_eq
532 [@prime_to_lt_SO @primeb_true_to_prime //
535 |#i #Hi1 #Hi2 @not_divides_to_dividesb_false
536 [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime //
537 |@(not_to_not … (lt_to_not_le x (exp p (S i)) ?))
538 [#H @divides_to_le // @(lt_to_le_to_lt ? p)
539 [@prime_to_lt_O @primeb_true_to_prime //
542 |@(lt_to_le_to_lt ? (exp p (S(log p x))))
543 [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
545 [@ prime_to_lt_O @primeb_true_to_prime //
556 (∏_{m < S n | leb p m ∧ dividesb (p\sup(S i)) m} p)))
557 [@(bigop_commute ?????? nat 1 timesAC (λm,i.p) ???) //
558 cut (p ≤ n) [@le_S_S_to_le //] #lepn
559 @(lt_O_log … lepn) @(lt_to_le_to_lt … lepn) @prime_to_lt_SO
560 @primeb_true_to_prime //
563 |#m #ltm #_ >exp_sigma @eq_f
565 (∑_{i < S n |leb 1 i∧dividesb (p\sup(S m)) i} 1))
568 cases (true_or_false (dividesb (p\sup(S m)) i)) #Hc >Hc
569 [cases (true_or_false (leb p i)) #Hp3 >Hp3
572 |@(transitive_le ? p)
573 [@prime_to_lt_O @primeb_true_to_prime //
580 @(not_to_not ??? (leb_false_to_not_le ?? Hp3)) #posi
581 @(transitive_le ? (exp p (S m)))
582 [>(exp_n_1 p) in ⊢ (?%?);
584 [@prime_to_lt_O @primeb_true_to_prime //
587 |@(divides_to_le … posi)
588 @dividesb_true_to_divides //
592 |cases (leb p i) cases (leb 1 i) //
596 |@eq_sigma_p_div @lt_O_exp
597 @prime_to_lt_O @primeb_true_to_prime //
609 theorem fact_pi_p2: ∀n. fact (2*n) =
610 ∏_{p < S (2*n) | primeb p}
612 (exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))).
613 #n >fact_pi_p @same_bigop
615 |#p #ltp #primep @same_bigop
617 |#i #lti #_ <exp_plus_times @eq_f
618 >commutative_times in ⊢ (???(?%?));
620 [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime //]
621 generalize in match (p ^(S i)); #a #posa
622 >(div_times_times n a 2) // >(commutative_times n 2)
623 <eq_div_div_div_times //
628 theorem fact_pi_p3: ∀n. fact (2*n) =
629 ∏_{p < S (2*n) | primeb p}
630 (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))) *
631 ∏_{p < S (2*n) | primeb p}
632 (∏_{i < log p (2*n)}(exp p (mod (2*n /(exp p (S i))) 2))).
633 #n <times_pi >fact_pi_p2 @same_bigop
635 |#p #ltp #primep @times_pi
639 theorem pi_p_primeb4: ∀n. 1 < n →
640 ∏_{p < S (2*n) | primeb p}
641 (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i))))))
643 ∏_{p < S n | primeb p}
644 (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))).
646 @sym_eq @(pad_bigop_nil … timesAC)
650 [>bigop_Strue // whd in ⊢ (??(??%)?); <times_n_1
651 <exp_n_1 >eq_div_O //
657 theorem pi_p_primeb5: ∀n. 1 < n →
658 ∏_{p < S (2*n) | primeb p}
659 (∏_{i < log p (2*n)} (exp p (2*(n /(exp p (S i))))))
661 ∏_{p < S n | primeb p}
662 (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))).
663 #n #lt1n >(pi_p_primeb4 ? lt1n) @same_bigop
665 |#p #lepn #primebp @sym_eq @(pad_bigop_nil … timesAC)
667 [@prime_to_lt_SO @primeb_true_to_prime //
670 |#i #lelog #lti %2 >eq_div_O //
671 @(lt_to_le_to_lt ? (exp p (S(log p n))))
672 [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
674 [@prime_to_lt_O @primeb_true_to_prime // |@le_S_S //]
680 theorem exp_fact_2: ∀n.
682 ∏_{p < S n| primeb p}
683 (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))).
684 #n >fact_pi_p <exp_pi @same_bigop
686 |#p #ltp #primebp @sym_eq
687 @(trans_eq ?? (∏_{x < log p n} (exp (exp p (n/(exp p (S x)))) 2)))
690 |#x #ltx #_ @sym_eq >commutative_times @exp_exp_times