no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N✝ : ℕ
τ✝ : ℝ
a✝ : SatelliteConfig E N✝ τ✝
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
⊢ r (centerAndRescale a) (last N) = 1
simp [SatelliteConfig.centerAndRescale, inv_mul_cancel (a.rpos _).ne']