Theorem le_eq_trans

Proof
01. 1 ⊢ a ≤ b, hypo.
02. 2 ⊢ b = c, hypo.
03. 1, 2 ⊢ a ≤ c, eq_subst 2 1, P t ↔ a ≤ t.
le_eq_trans. ⊢ a ≤ b → b = c → a ≤ c, subj_intro_ii 3.

Dependencies
The given proof depends on one axiom:
eq_subst.