proposition: Lemma linear_injective_lt_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)) -> lt (target u) (ev u x) (ev u y) -> lt (source u) x y.
proof: Proof. intros. unfold lt in H4. unfold lt in |- *; ee. apply linear_injective_leq_back; au. unfold not in |- *; intros. apply H5. rewrite H6; tv. Qed.
imports: universe