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