Mathlib GenContFract.of x is the Gauss-map orbit: linking lemmas

For a.e. statements about continued fraction digits, do not reimplement digits. Prove that GenContFract.IntFractPair.stream x n = some ⟨b, T^[n] (Int.fract x)⟩ with T y = Int.fract y⁻¹, by induction using IntFractPair.stream_succ_of_some (needs fr ≠ 0, true for irrational x). Then GenContFract.get?_of_eq_some_of_succ_get?_intFractPair_stream gives (of x).s.get? n = some ⟨1, ⌊(Tⁿ fract x)⁻¹⌋⟩. Next, partDens = s.map Pair.b: rewrite with Stream'.Seq.map_get? (import Mathlib.Data.Seq.Basic, otherwise 'unknown constant'). For denominators, induct on the pair (dens n, dens (n+1)) with GenContFract.zeroth_den_eq_one, first_den_eq, dens_recurrence. To move from Gauss-measure-a.e. to Lebesgue-a.e. on ℝ, use withDensity_absolutelyContinuous' (Lebesgue|(0,1] ≪ Gauss) and Int.preimage_fract + measure_preimage_add_right, which pull null sets back through fract. Side gotcha: decide cannot prove ¬IsSquare 6 (it gets stuck on Nat.sqrt), but decide +kernel can.