a=?b =false-> b=?a =false. To prove this which command i should apply?

You may search into Coq's library the lemma about commutativity of Boolean comparison.

```
Search ((?x =? ?y) = (?y =? ?x)).
Goal forall a b, a=?b = false -> b=?a = false.
intros a b; rewrite Nat.eqb_sym; easy.
Qed.
```

I thought `lia`

meanwhile does support boolean relational operators, but apparently it doesn't.

Last updated: Oct 04 2023 at 23:01 UTC