proposition: Lemma scale_subset_union : forall a z:E, is_well_ordered a -> (forall y:E, inc y z -> scale_subset y a) -> scale_subset (union z) a.
proof: Proof. ir. uhg. ee. am. ap union_sub. ir. cp (H0 _ H1). uh H2. ee. am. ir. cp (union_exists H1). nin H3. ee. cp (H0 _ H4). uh H5; ee. apply union_inc with x0. apply H7 with y. am. am. am. Qed.
imports: Arith order