Various lemmas about size of Doc

These will be helpful for termination proofs. They will be used implicitly, as we mark them with @[simp].

ink

@[simp]

theorem Doc.size_choice₁ {d₁ : Doc} {d₂ : Doc} : Doc.size d₁ < Doc.size (Doc.choice d₁ d₂)

ink

@[simp]

theorem Doc.size_choice₂ {d₂ : Doc} {d₁ : Doc} : Doc.size d₂ < Doc.size (Doc.choice d₁ d₂)

ink

@[simp]

theorem Doc.size_align {d' : Doc} : Doc.size d' < Doc.size (Doc.align d')

ink

@[simp]

theorem Doc.size_nest {d' : Doc} {n : ℕ} : Doc.size d' < Doc.size (Doc.nest n d')

ink

@[simp]

theorem Doc.size_concat₁ {d₁ : Doc} {d₂ : Doc} : Doc.size d₁ < Doc.size (Doc.concat d₁ d₂)

ink

@[simp]

theorem Doc.size_concat₂ {d₁ : Doc} {d₂ : Doc} : Doc.size d₂ < Doc.size (Doc.concat d₁ d₂)