How can this be solved?

```
Require Import Arith ssreflect.
Goal forall a b: nat,
(if a <=? b then false else true) = true -> a <= b.
Proof.
```

It is possible, right? Since we are going from decidable inequality to a Prop version.

`if x then false else true`

amounts to the boolean negation of `x`

, so your statement looks wrong. Besides, unless you import libraries that contain something linking `<=?`

and `<=`

, you will probably use induction.

Best use lemmas like Nat.leb_le or Nat.leb_spec; they should be imported by Require Arith

Last updated: Jun 13 2024 at 19:02 UTC