Document `strong_coinduct`

In lean4#14855 a support for strong coinduction was added. For example:

coinductive infSeq {r : α → α → Prop} : α → Prop where
  | mk : r a b → infSeq b → infSeq a

/--
info: infSeq.coinduct.{u_1} {α : Sort u_1} {r : α → α → Prop} (pred : α → Prop)
  (hyp : ∀ (a : α), pred a → ∃ b, r a b ∧ pred b) (a✝ : α) : pred a✝ → infSeq a✝
-/
#guard_msgs in
#check infSeq.coinduct

/--
info: infSeq.strong_coinduct.{u_1} {α : Sort u_1} {r : α → α → Prop} (pred : α → Prop)
  (hyp : ∀ (a : α), pred a → ∃ b, r a b ∧ (pred b ∨ infSeq b)) (a✝ : α) : pred a✝ → infSeq a✝
-/
#guard_msgs in
#check infSeq.strong_coinduct

Note, that this also works for mutually-recursive (including mixed inductive-coinductive) definitions.

Start with the reference manual section covering coinductive definitions and use the issue's infSeq example and #check output as the documentation requirements. Document strong_coinduct, including its hypothesis and applicability to mutually recursive and mixed inductive-coinductive definitions; done when these cases are clearly explained with the relevant example.