Proof 01. 1 ⊢ a < b, hypo. 02. 1 ⊢ ¬a = b, lsubj_conj_elimr lt_equi 1. neq_from_lt. ⊢ a < b → ¬a = b, subj_intro 2.