simp? says simp only [isUnit_one, IsUnit.dvd, Nat.isUnit_iff, Nat.dvd_one, true_and]
I : BasicInterval
⊢ 1 ∣ I.a₂ * I.b₁ ∧ 1 ∣ I.a₁ * I.b₂ ∧ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c ∣ 1
I : BasicInterval
⊢ ∀ (c : ℕ), c ∣ I.a₂ * I.b₁ → c ∣ I.a₁ * I.b₂ → c = 1