Dear Julian,

this would be easier to answer if you would give more information on where your “Int” module comes from. It looks quite like (https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v) but in the version I am using (3.5 and master) there is no `le`

function. Without knowing what library you are using one cannot tell what facilities this library might have to solve such goals. Easiest (and most polite) is to supply a snippet of Coq code which can be run + information on versions you are using.

In case you are using something similar to the CompCert Integers library, a good way to do partial simplifications on constant terms is the change tactic, which can replace any terms which eventually compute to the same thing. cbn in H does nothing and compute in H probably doesn’t give you what you want. With change you get this far on a simplified goal (because I don’t have le):

```
Require Import compcert.lib.Integers.
Require Import ZArith.
Require Import Bool.
Goal
forall (tlbe0:int),
forall (ea:int),
(if (Int.eq (Int.repr 255) (Int.repr 255)
|| Int.eq (Int.repr 255) Int.zero) &&
Int.eq (Int.shru (Int.repr 1048576) (Int.repr 6))
(Int.and (Int.shru ea (Int.repr 16)) (Int.repr 65535))
then Some tlbe0
else None) = None
->
False.
Proof.
intros.
change (Int.eq (Int.repr 255) (Int.repr 255)) with true in H. cbn in H.
change (Int.shru (Int.repr 1048576) (Int.repr 6)) with (Int.repr 16384) in H.
```

results in

```
1 subgoal
tlbe0, ea : int
H : (if Int.eq (Int.repr 16384) (Int.and (Int.shru ea (Int.repr 16)) (Int.repr 65535))
then Some tlbe0
else None) = None
______________________________________(1/1)
False
```

I am not aware of any automated tool which can handle inequalities and bit operations, so I guess you have to see what `Search Int.shru`

gives you. May be you can convert the shru to a division in Nat or Z and convert the goal with ring tactics to something lia can solve. But I would think this is a common thing for you, so I would prove some useful lemmas for this.

Best regards,

Michael