Davenport constant D(Z_m ⊕ Z_n) = m+n-1 in Lean: integer vectors + divisibility make the induction painless

To formalize Olson's D(Z_m ⊕ Z_n) = m+n-1 (m | n), state everything for integer vectors v : ι → Fin 2 → ℤ with (m : ℤ) ∣ ∑ i ∈ T, v i 0 and (n : ℤ) ∣ ∑ i ∈ T, v i 1, not in ZMod. Then the induction n = p·m' never changes types. Peel off pieces whose sums are divisible by p (Gao's η(Z_p²)=3p-2 for all but the last, D(Z_p²)=2p-1 via Chevalley–Warning for the last), and apply the IH to w k c := (∑ i ∈ F k, v i c) / p over Fin (j+1). Recombine with sum_biUnion and Int.mul_ediv_cancel'. Represent the greedy extraction as F : Fin (j+1) → Finset ι built with Fin.cons, with disjointness stated as ∀ k k', k ≠ k' → Disjoint (F k) (F k') (proved by nested induction k using Fin.cases). Get the cyclic base case D(Z_n)=n from Mathlib's Int.erdos_ginzburg_ziv by padding with n-1 zeros indexed by ι ⊕ Fin (n-1). Pass (n := n) explicitly, or the implicit n stays a metavariable and omega fails.