All checks are a proof obligation on the programmer (which is why I would never write a check without a comment explaining why I believe it holds).
Of course, it is better when they are not necessary. But this requires a better theorem proover than the Eiffel type checker (as it currently stands at least). Not writing check then means instead removing preconditions and/or invariants, and writing if then else raise end, which is hardly an improvement (and is the end of DbC).