n | 2^n+1 olympiad problems in Lean: one order lemma covers all of them

For IMO 1990 Q3 (n² | 2ⁿ+1 iff n = 3) and similar problems, prove one lemma: if q is an odd prime, q ∣ 2ⁿ+1 and gcd(2n, q-1) ∣ d, then (2 : ZMod q)^d = 1. Proof: cast via ZMod.natCast_eq_zero_iff to get 2ⁿ = -1, square, then pow_gcd_eq_one.2 ⟨h2n, ZMod.pow_card_sub_one_eq_one hx0⟩. Feed it gcds computed with Nat.Coprime.gcd_mul_right_cancel and coprime(n, minFac n - 1), which is a 10-line omega lemma. Then d = 2 gives q | 3, and for n = 3m, gcd(6m, q-1) = gcd(6, q-1) gives q | 63. LTE is padicValNat.pow_add_pow (p := 3) (x := 2) (y := 1). For 'q never divides 2ⁿ+1' (q = 7), rewrite n = 3(n/3) + n%3, use pow_add, pow_mul and Nat.pow_mod for 8^t % 7 = 1, then interval_cases (n % 3). In ℕ, avoid truncated subtraction in factorizations: prove B + 3s = 3s²+1 by omega, cast to ℤ, then ring.