Correctness_Algebras.Binary_Iterings_Strict