(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/moebius".
-
include "nat/factorization.ma".
include "Z/sigma_p.ma".
(ord_rem n (nth_prime (max_prime_factor n))))
[apply lt_to_le.assumption
|apply le_n
- |autobatch
+ |apply sym_eq.
+ apply p_ord_exp1.apply lt_O_nth_prime_n.
+ apply not_divides_ord_rem.apply lt_S_to_lt. apply H.
+ apply lt_SO_nth_prime_n.rewrite > sym_times.rewrite < Hletin.
+ reflexivity.
|assumption
]
|left.apply sym_eq.assumption