have : step n ≃ m * q + r := calc
  step n             ≃ _ := AA.subst₁ ‹n ≃ m' * q + r'›
  step (m' * q + r') ≃ _ := Rel.symm Natural.add_step
  m' * q + step r'   ≃ _ := AA.substR ‹step r' ≃ q›
  m' * q + q         ≃ _ := Rel.symm Natural.step_mul
  step m' * q        ≃ _ := Rel.symm Natural.add_zero
  step m' * q + 0    ≃ _ := Rel.refl
  m * q + r          ≃ _ := Rel.refl
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝² : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝¹ : step r' ≤ q
this✝ : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
this : r < q
⊢ Euclid (step n) q
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝³ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝² : step r' ≤ q
this✝¹ : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
this✝ : r < q
this : step n ≃ m * q + r
⊢ Euclid (step n) q