proposition: Lemma lgs_limit_or_tack : forall (f:E1)(y:E), is_leq_gen_scale f y -> (exists z:E, ((forall x:E, inc x z -> (is_leq_gen_scale f x & strict_sub x y)) & y = union z)) \/ (exists x :E, (is_leq_gen_scale f x & y = tack_on x (f x))& ~inc (f x) x).
proof: Proof. ir. pose (z:= Z (powerset y) (fun x:E=> (is_leq_gen_scale f x & strict_sub x y))). pose (w:= union z). assert (sub w y). uhg; ir. ufi w H0; cp (union_exists H0). nin H1; ee. ufi z H2; Ztac. uh H5; ee. ap H6; am. assert (is_leq_gen_scale f w). uf w. ap leq_gen_scale_union. ir. ufi z H1; Ztac; am. apply by_cases with (w = y); ir. ap or_introl; sh z; ee; ir. ufi z H3; Ztac. wr H2; tv. ap or_intror; sh w; ee. am. ap excluded_middle; uhg; ir. assert (~sub (tack_on w (f w)) w). uhg; ir. cp H; uh H; nin H; ee. assert (strict_sub w y). uhg; ee; am. apply next_not_inc with x w. rw H; am. uh H6; ee; am. util (next_compatible_scale (f:=f) (a:=x) (y:=w)). am. apply leq_gen_scale_subset with f. am. am. rw H; am. rw H; am. rw H8. ap H4. rw tack_on_inc. ap or_intror; tv. ap H4. uhg; ir. uf w; apply union_inc with (tack_on w (f w)). am. assert (sub (tack_on w (f w)) y). assert (strict_sub w y). uhg; ee; am. cp H. uh H7; nin H7; ee. util (next_compatible_scale (f:=f) (a:= x0) (y:= w)). am. apply leq_gen_scale_subset with f. am. am. rw H7; am. rw H7; am. uhg; ir. rwi tack_on_inc H10; nin H10. ap H0; am. rw H10. wr H9. wr H7. ap next_inc_U. rw H7; am. uh H8; ee; am. uf z; ap Z_inc. ap powerset_inc. am. ee. apply by_cases with (inc (f w) w); ir. assert (tack_on w (f w) = w). ap extensionality; uhg; ir. rwi tack_on_inc H8; nin H8. am. rw H8; am. rw tack_on_inc; ap or_introl; am. rw H8. am. ap leq_gen_scale_tack_on. am. am. uhg; ee. uhg; uhg; ir. ap H3; sy; am. am. cp H; uh H; nin H; ee. util (next_compatible_scale (f:=f) (a:= x) (y:= w)). am. apply leq_gen_scale_subset with f. am. am. rw H; am. rw H; uhg; ee; am. wr H5. ap next_not_inc. rw H; uhg; ee; am. uh H4; ee; am. Qed.
imports: Arith order