proposition: Lemma scale_subset_union_exists : forall a z u v : E, is_well_ordered a -> (forall y: E, inc y z -> scale_subset y a) -> inc u (union z) -> inc v (union z) -> exists y : E, (inc y z & scale_subset y a & inc u y & inc v y).
proof: Proof. ir. cp (union_exists H1). cp (union_exists H2). nin H3. nin H4. ee. assert (sub x x0 \/ sub x0 x). apply scale_subset_or with a. ap H0; am. ap H0; am. nin H7. sh x0. xd. sh x. xd. Qed.
imports: Arith order