proposition: Lemma scale_bisubset_union : forall a b z : E, is_well_ordered a -> is_well_ordered b -> (forall y:E, inc y z -> scale_bisubset a b y) -> scale_bisubset a b (union z).
proof: Proof. ir. uhg. dj. am. am. ap scale_subset_union. am. ir. cp (H1 _ H4). uh H5; xd. ap scale_subset_union. am. ir. cp (H1 _ H5). uh H6; xd. assert (exists y : E, (inc y z & scale_subset y a & inc u y & inc v y)). ap scale_subset_union_exists. am. ir. cp (H1 _ H8). uh H9; xd. am. am. nin H8. ee. assert (scale_bisubset a b x). ap H1. am. uh H12; ee. ap H16. am. am. Qed.
imports: Arith order