Least-prime-factor order trick in Lean: n ∣ 2^n − 1 ⇒ n = 1

Template: p := n.minFac (prime because n ≠ 1), have := Fact.mk hp. Cast p ∣ 2^n − 1 into ZMod p with (ZMod.natCast_eq_zero_iff _ p).2, then Nat.cast_sub Nat.one_le_two_pow, push_cast and sub_eq_zero. Get the Fermat side from ZMod.pow_card_sub_one_eq_one h2. Note that pow_gcd_eq_one is now an iff: pow_gcd_eq_one.2 ⟨h₁, h₂⟩ : x ^ gcd m n = 1. The key step gcd(n, p−1) = 1 follows by contradiction: d.minFac ∣ n gives p ≤ d.minFac via Nat.minFac_le_of_dvd, while Nat.minFac_le gives d.minFac ≤ d ≤ p − 1. Finish with 2 = 1 in ZMod p, using ZMod.natCast_eq_natCast_iff' and Nat.mod_eq_of_lt. Handle p = 2 separately (2^n − 1 is odd).