proposition: Lemma downward_lgs_minimal : forall (f:E1)(x y:E), is_leq_gen_scale f y -> inc x y -> sub (downward_lgs f x) y.
proof: Proof. ir. cp H. uh H1; nin H1; ee. assert (lem1:leq_gen f x x). rewrite leq_gen_leq with (a:=x0). ap leq_refl. do 3 (uh H2; ee); am. rw H1; am. am. rw H1; am. rw H1; am. pose (u:= downward_lgs f x). assert (is_leq_gen_scale f u). uf u; ap downward_lgs_lgs. am. cp H3. uh H4; nin H4; ee. nin (leq_gen_scale_or H H3). assert (scale_subset y x1). apply leq_gen_scale_subset with f. am. am. rw H4; am. uf u; uf downward_lgs; uhg; ir; Ztac. clear H8. apply leq_gen_scale_saturated with f x. am. am. am. am. Qed.
imports: Arith order