Correctness_Algebras.Binary_Iterings_Nonstrict