Sub l Infty Norm le

theorem sub_lInftyNorm_le {cols : ℕ} (v w : PolyVec (Rq Φ) cols) {bound : ℕ}    (hv : vecLInftyNorm Φ v ≤ bound) (hw : vecLInftyNorm Φ w ≤ bound) :    vecLInftyNorm Φ (v - w) ≤ subLInftyNormBound bound := by  have hstep : vecLInftyNorm Φ (v - w) ≤ vecLInftyNorm Φ v + vecLInftyNorm Φ w := by    unfold vecLInftyNorm    refine Finset.sup_le (fun i _ => ?_)    simp only [Pi.sub_apply]    calc Rq.lInftyNorm Φ (v i - w i)        ≤ Rq.lInftyNorm Φ (v i) + Rq.lInftyNorm Φ (w i) := Rq.lInftyNorm_sub_le Φ _ _      _ ≤ (Finset.univ : Finset (Fin cols)).sup (fun i => Rq.lInftyNorm Φ (v i))            + (Finset.univ : Finset (Fin cols)).sup (fun i => Rq.lInftyNorm Φ (w i)) :=          add_le_add            (Finset.le_sup (f := fun i => Rq.lInftyNorm Φ (v i)) (Finset.mem_univ i))            (Finset.le_sup (f := fun i => Rq.lInftyNorm Φ (w i)) (Finset.mem_univ i))  unfold subLInftyNormBound  omega