proposition: Lemma injective_lt_lt : forall u x y : E, mor_axioms u -> injective u -> lt (source u) x y -> lt (target u) (ev u x) (ev u y).
proof: Proof. ir. ufi lt H1. uf lt; ee. ufi mor_axioms H; xe. ap H5. am. uf not; intros. ufi injective H0; ee. ufi Transformation.injective H4. ee. ufi Transformation.injects H5. ap H2. ap H5. ufi mor_axioms H; ee. ufi axioms H; ee. apply H9 with y. am. ufi mor_axioms H; ee. ufi axioms H; ee. apply H10 with x; au. am. Qed.
imports: universe