proposition: Lemma linear_injective_leq_back : forall u x y : E, mor_axioms u -> injective u -> is_linear (source u) -> inc x (U (source u)) -> inc y (U (source u)) -> leq (target u) (ev u x) (ev u y) -> leq (source u) x y.
proof: Proof. intros. apply linear_not_lt_leq; au. intros. pose (injective_lt_lt H H0 H5). apply no_lt_leq with (target u) (ev u y) (ev u x). assert (mor_axioms u). am. unfold mor_axioms in H6; ee. am. am. am. Qed.
imports: universe