proposition: Lemma lgs_smallest_with_property : forall (f:E1)(p:EP), (exists y:E, (is_leq_gen_scale f y & p y)) -> exists x : E, (is_leq_gen_scale f x & p x & (forall y :E, is_leq_gen_scale f y -> p y -> sub x y)).
proof: Proof. ir. nin H; ee. cp H; uh H; nin H; ee. apply by_cases with (exists y:E, (strict_sub y x & is_leq_gen_scale f y & p y)); ir. pose (b := Z x (fun v:E=> p (punctured_downward_subset x0 v))). assert (sub b (U x0)). rw H; uf b; uhg; ir; Ztac. assert (nonempty b). nin H3. ee. assert (scale_subset x1 x0). apply leq_gen_scale_subset with f. am. am. rw H; uh H3; ee; am. sh (next x0 x1). uf b; ap Z_inc. wr H; ap next_inc_U. rw H; am. uh H2; ee; am. rw scale_is_punctured_downward. am. am. rw H; am. cp H2. uh H6; ee. uh H6; ee. nin (H8 b H4 H5). sh (punctured_downward_subset x0 x1). dj. apply scale_subset_is_leq_gen_scale with x0. am. ap punctured_downward_scale. uh H2; ee; am. uh H9; ee. ap H4; am. uh H9; ee. ufi b H11; Ztac. nin (leq_gen_scale_or H1 H12). uhg; ir; ap H14. wr H; ufi punctured_downward_subset H15; Ztac. pose (w:= next x0 y). assert (scale_subset y x0). apply leq_gen_scale_subset with f. am. am. rw H; am. apply by_cases with (y=x); ir. rw H16; wr H; uf punctured_downward_subset; uhg; ir; Ztac. assert (y= punctured_downward_subset x0 w). sy; uf w; ap scale_is_punctured_downward. am. uhg; ee. rw H; am. rw H; am. assert (inc w b). uf b; ap Z_inc. wr H; uf w; ap next_inc_U. uhg; ee. rw H; am. rw H; am. uh H2; ee; am. wr H17; am. assert (leq x0 x1 w). uh H9; ee. uh H9; ee. ap H22. am. uhg; ir. ufi punctured_downward_subset H20; Ztac; ee. rw H17; uf punctured_downward_subset; ap Z_inc. am. apply lt_leq_trans with x1. do 3 (uh H2; ee); am. am. am. sh x. ee. am. am. ir. nin (leq_gen_scale_or H1 H4). am. apply by_cases with (y = x). ir. rw H7; uhg; ir; am. ir. assert False. ap H3. sh y. ee. uhg; ee; am. am. am. elim H8. Qed.
imports: Arith order