LLVM can't see an always-true relationship between two divided numbers:

void check(unsigned long v) { assert((v / 100) <= v); // optimized out OK assert((v / 200) <= v); // optimized out OK assert((v / 200) <= (v / 2)); // FAIL  }

Oddly, adding if (v >= 400) return; makes it prove the third case is true:

void check(unsigned long v) { if (v >= 400) return; assert((v / 100) <= v); // optimized out assert((v / 200) <= v); // optimized out assert((v / 200) <= (v / 2)); // optimized out now too  }

but with if (v >= 401) return; it becomes unknowable again.

Here's a real-world code that needs such reasoning to remove bounds checks:

https://github.com/kornelski/rust/blob/999967a57dce987bbad353d152f03c3ef67d41f2/library/core/src/slice/sort/select.rs#L222-L232

I expected I'd only need to prove the v.len() is non-0 to remove the bounds checks, but I needed to add more hints.