Proving inequality equivalence using propositional logic: stuck with redundancy at the end of the proof + circularity problem

Question

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)

Answer 1

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.