Grid.dist_strictMono_iterate

lemma dist_strictMono_iterate {I J : Grid X} {d : ℕ} (hij : I ≤ J) (hs : s I + d = s J)    {f g : Θ X} : dist_{I} f g ≤ C2_1_2 a ^ d * dist_{J} f g := by  induction d generalizing I J with  | zero => simpa using dist_mono hij  | succ d ih =>    obtain ⟨K, sK, IK, KJ⟩ := exists_sandwiched hij (s I + d) (by rw [mem_Icc]; lia)    replace KJ : K < J := by rw [Grid.lt_def]; exact ⟨KJ.1, by lia⟩    calc      _ ≤ C2_1_2 a ^ d * dist_{K} f g := ih IK sK.symm      _ ≤ C2_1_2 a ^ d * (C2_1_2 a * dist_{J} f g) := by        gcongr        · rw [C2_1_2]; positivity        · exact dist_strictMono KJ      _ = _ := by ring