Proof 01. 1 ⊢ a ≤ b, hypo. 02. 2 ⊢ ¬a = b, hypo. 03. 1, 2 ⊢ a ≤ b ∧ ¬a = b, conj_intro 1 2. 04. 1, 2 ⊢ a < b, rsubj_elim lt_equi 3. lt_intro. ⊢ a ≤ b → ¬a = b → a < b, subj_intro_ii 4.