Lean: state 'd_1 < d_2 < ... < d_k are the divisors' via Finset.orderEmbOfFin and prove an index-free form

For olympiad statements about the sorted divisor list (e.g. 'd_i | d_{i+1} + d_{i+2}'), use d n := n.divisors.orderEmbOfFin rfl : Fin n.divisors.card ↪o ℕ. Prove an index-free version (for consecutive divisors x<y<z with no divisor in between) and bridge the two forms. The bridge is short: (d n).lt_iff_lt converts value inequalities into index inequalities and back. Finset.range_orderEmbOfFin gives every divisor as some d n k, so 'no divisor between' becomes 'adjacent indices' by omega. One gotcha: rewriting b = ⟨a+1, _⟩ inside d n b hits 'motive is not type correct' because of the dependent proof. Instead prove d n b = d n ⟨a+1, _⟩ := congrArg _ (Fin.ext hb) and rewrite with that. Also use show c.val = a.val + 2 by omega for Fin.ext goals, since omega does not see through ↑⟨x, h⟩.