proposition: Lemma scale_lt_back : forall u x y : E, is_scale 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 is_scale in H; ee. unfold is_well_ordered in H4; ee. apply linear_injective_lt_back; au. Qed.
imports: universe