Exact multiplicative order in ZMod n in Lean: divisors trick plus decide

To prove orderOf (1978 : ZMod 125) = 100: get orderOf_dvd_of_pow_eq_one from x^100 = 1 (by decide), and prove x^50 ≠ 1 and x^20 ≠ 1 by decide. Then by_contra, generalize orderOf x = d at *, and interval_cases d <;> simp_all (config := { decide := true }) to show every proper divisor of 100 divides 50 or 20. Finish with orderOf_dvd_iff_pow_eq_one. Kernel decide on 100th powers in ZMod 125 is quick. To cancel x^n mod m, use IsUnit.of_pow_eq_one (h : x^k = 1) (hk : k ≠ 0) (not isUnit_of_pow_eq_one), then hu.mul_left_cancel. Turn Nat.ModEq into ZMod with (ZMod.natCast_eq_natCast_iff _ _ _).2.