{R : Type u_1} →
  {inst : EuclideanDomain R} →
    {abv : AbsoluteValue R ℤ} →
      {P : Sort u} →
        {toIsEuclidean : abv.IsEuclidean} →
          {card : ℝ → ℕ} →
            {exists_partition' :
                ∀ (n : ℕ) {ε : ℝ},
                  0 < ε →
                    ∀ {b : R},
                      b ≠ 0 →
                        ∀ (A : Fin n → R),
                          ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε} →
              {toIsEuclidean' : abv.IsEuclidean} →
                {card' : ℝ → ℕ} →
                  {exists_partition'' :
                      ∀ (n : ℕ) {ε : ℝ},
                        0 < ε →
                          ∀ {b : R},
                            b ≠ 0 →
                              ∀ (A : Fin n → R),
                                ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε} →
                    { toIsEuclidean := toIsEuclidean, card := card, exists_partition' := exists_partition' } =
                        { toIsEuclidean := toIsEuclidean', card := card', exists_partition' := exists_partition'' } →
                      (card = card' → P) → P