Correctness_Algebras.Binary_Iterings