Coq formalization of guarded iteration a la https://www8.cs.fau.de/_media/research:papers:elgot-retract.pdf.