El invariante sobrevive a cada iteración

Cambia los datos y avanza una iteración. La igualdad verde debe seguir siendo verdadera desde el inicio hasta la salida.

Iteraciones ejecutadas
Invariante