Proof 01. 1 ⊢ a < b, hypo. 02. 1 ⊢ a ≤ b, lsubj_conj_eliml lt_equi 1. le_from_lt. ⊢ a < b → a ≤ b, subj_intro 2.