We would like to report an error in a proof given by J.-P. Verjus in . More importantly, we would like to point out a difference between the notions "always-true" and "invariant", which are identified in . In his paper, Verjus claims that invariance proofs by contradiction are shorter than invariance proofs by the established method, called the "induction method" in . To illustrate his idea, he proposes an alternative correctness proof for a termination detection algorithm given by Dijkstra, Feijen, and Van Gasteren . We show that his—operational—proof is incorrect and incomplete (Section 1); moreover, what he shows is that a predicate is always-true, which is strictly weaker than invariance (Section 2). Instead of illustrating the merits of proofs by contradiction, the proof strongly supports our opinion that operational arguments should be avoided.