Proving inequality equivalence using propositional logic: stuck with redundancy at the end of the proof + circularity problem I would like to prove formally that : ~ ( a is less than b or equal to b) is equivalent to ( a is strictly greater than b ). But I cannot get rid of a redundant conjoint at the end of the proof. Other problem: at line (3) I seem obliged to admit trichotomy law. But is not assuming this law tentamount to reasoning circularly? Which proposition should be taken as primitive in order not to fall into circularity? ~ ( a is strictly less than b OR a is equal to b) <==> ~ (a < b) & ~(a = b) <==> (a > b or a = b) & ~( a = b) <==> (a > b & ~ a = b ) OR ( a=b & ~ a = b) <==> (a > b & ~ a = b) OR FALSE <==> (a > b & ~ a=b)

But **it is** trichotomy law :

> $(a < b \lor a=b \lor a > b)$.

Rewrite it as : $(a < b \lor a=b) \lor (a > b)$ and using Material Implication rule) we get :

> $\lnot (a < b \lor a=b) \to (a > b)$.

And vice versa.