proposition: Lemma downward_lgs_inc : forall (f:E1)(x y:E), leq_gen f x x -> inc y (downward_lgs f x) = leq_gen f y x.
proof: Proof. ir. ap iff_eq; ir. ufi downward_lgs H0; Ztac. uf downward_lgs; ap Z_inc. pose (u:=choose_lgs_containing f x). assert (is_leq_gen_scale f u & inc x u). uf u. uf choose_lgs_containing. pose (p:=fun y0 : E => is_leq_gen_scale f y0 & inc x y0). assert (ex p). sh (downward_lgs f x). uf p; cbv beta. ee. ap downward_lgs_lgs. am. ap downward_lgs_inc_refl. am. cp (choose_pr H1). exact H2. apply leq_gen_scale_saturated with f x. am. ee; am. ee; am. am. Qed.
imports: Arith order