Resumptions, Weak Bisimilarity and Big-Step Semantics for While With Interactive I/O: An Exercise in Mixed Induction-Coinduction