proposition: Lemma leq_gen_scale_union : forall (f:E1)(z:E), (forall y:E, inc y z -> is_leq_gen_scale f y) -> is_leq_gen_scale f (union z).
proof: Proof. ir. uhg. pose (a:= create (union z) (leq_gen f)). sh a. dj. uf a; ap underlying_create. uhg; dj. uhg; dj. uhg; dj. uf a; ap create_axioms. uhg; ee. ir. cp (union_exists H1). nin H2. ee. cp (H _ H3). uh H4; nin H4; ee. assert (leq x1 x x = leq_gen f x x). sy. ap leq_gen_leq. am. rw H4; am. rw H4; am. wr H6. ap leq_refl. do 3 (uh H5; ee); am. rw H4; am. ir. apply leq_gen_eq with f. am. am. ir. apply leq_gen_trans with y; am. assert (leq a x x & leq a y y). ee; ap leq_refl; am. ufi a H4. do 2 (rwi leq_create_all H4); ee. cp (leq_gen_or H9 H8). nin H10. ap or_introl. uf a; rw leq_create. am. am. am. ap or_intror. uf a; rw leq_create; am. assert (exists t:E, (inc t b & (forall x:E, inc x b -> leq_gen f t x))). ap leq_gen_bottom_elt. ir. assert (inc x (U a)). ap H2; am. ufi a H5. rwi underlying_create H5. cp (union_exists H5). nin H6; ee. cp (H _ H7). uh H8; nin H8; ee. wri H8 H6. cp (leq_gen_leq H9 H6 H6). rw H10. ap leq_refl. do 3 (uh H9; ee); am. am. am. nin H4; ee. sh x. uhg; ee. uhg; ee. uh H1; ee; am. am. ap H2; am. ir. uf a. rw leq_create_all; ee. wr H0; ap H2; am. wr H0; ap H2; am. ap H5. am. am. rwi H0 H2. cp (union_exists H2). nin H3; ee. cp (H _ H4). cp H5. uh H5; nin H5; ee. assert (punctured_downward_subset a y = punctured_downward_subset x0 y). uf punctured_downward_subset; ap extensionality; uhg; ir; Ztac; ap Z_inc. rwi H0 H9. cp (union_exists H9). nin H11; ee. cp (H _ H12). cp (leq_gen_scale_or H6 H13). nin H14. uh H13; nin H13; ee. assert (scale_subset x x3). apply leq_gen_scale_subset with f. am. am. rw H13; am. rw H5. uh H16; ee. apply H18 with y. am. rewrite<- leq_gen_leq with (f:=f). uh H10; ee. ufi a H10; rwi leq_create_all H10; ee; am. am. rw H13; am. rw H13; ap H14; am. rw H5; ap H14; am. uh H10; ee. uhg; ee; try am. rewrite <- leq_gen_leq with (f:=f). ufi a H10; rwi leq_create_all H10; ee; am. am. rwi H0 H9. cp (union_exists H9). nin H12; ee. cp (H _ H13). cp (leq_gen_scale_or H6 H14). nin H15. uh H14; nin H14; ee. assert (scale_subset x x3). apply leq_gen_scale_subset with f. am. am. rw H14; am. rw H5. uh H17; ee. apply H19 with y. am. rewrite<- leq_gen_leq with (f:=f). ufi a H10; rwi leq_create_all H10; ee; am. am. rw H14; am. rw H14; ap H15; am. rw H5; ap H15; am. rw H5; am. rw H0. apply union_inc with x. wr H5; am. am. uh H10; ee. uhg; ee; try am. uf a; rw leq_create_all; ee. apply union_inc with x. wr H5; am. am. apply union_inc with x; am. rewrite leq_gen_leq with (a:= x0). am. am. am. rw H5; am. rw H8. uh H7; ee. ap H9. rw H5; am. Qed.
imports: Arith order