exact lt_of_le_of_lt (Nat.le_of_dvd  (Nat.sub_pos_of_lt <| h2q) h_piv_div_q_sub_one)
    <| pred_lt <| Nat.ne_of_gt <| Nat.le_of_lt h2q
case h.right
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
h2q : 2 ≤ q
⊢ p < q
no goals