proposition: Lemma lt_leq_trans : forall a x y z : E, axioms a -> lt a x y -> leq a y z -> lt a x z.
proof: Proof. ir. uf lt; ufi lt H0; ee. ufi axioms H; ee. apply H6 with y; au. uf not; ir. rwi H3 H0. ufi axioms H; ee. ap H2. rw H3. ap H6; au. Qed.
imports: universe