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