proposition: Lemma downward_lgs_lgs : forall (f:E1)(x:E), leq_gen f x x -> is_leq_gen_scale f (downward_lgs f x).
proof: Proof. ir. pose (u:= choose_lgs_containing f x). assert (is_leq_gen_scale f u & inc x u). rwi leq_gen_char H; ee. cp (choose_pr H). cbv beta in H1. ee. am. cp (choose_pr H); cbv beta in H1; ee; am. ee. uh H0; nin H0; ee. pose (a:= downward_suborder x0 x). uhg; sh a; ee. uf a; uf downward_suborder. rw underlying_suborder. uf downward_subset; uf downward_lgs; ap extensionality; uhg; ir; Ztac; ap Z_inc. fold u. wr H0; am. rewrite leq_gen_leq with (a:=x0). am. am. am. rw H0; am. rw H0; uf u; am. rewrite <- leq_gen_leq with (f:=f). am. am. rw H0; uf u; am. rw H0; am. uhg; dj. uf a; uf downward_suborder; ap suborder_well_ordered. uf downward_subset. uhg; ir; Ztac. uh H2; ee; am. assert (punctured_downward_subset a y = punctured_downward_subset x0 y). assert (sub (U a) (U x0)). uhg; ir. ufi a H5; ufi downward_suborder H5; rwi underlying_suborder H5. ufi downward_subset H5; Ztac. assert (forall r s:E, leq a r s -> leq x0 r s). ir. ufi a H6; ufi downward_suborder H6; rwi leq_suborder_all H6. ee. am. do 3 (uh H2; ee). am. uf downward_subset; uhg; ir; Ztac. assert (ax: axioms x0). do 3 (uh H2; ee); am. assert (lem1 : leq x0 y x). ufi a H4; ufi downward_suborder H4; rwi underlying_suborder H4; ufi downward_subset H4; Ztac. assert (forall r s : E, leq x0 r s -> leq x0 s x -> leq a r s). ir. uf a. uf downward_suborder. rw leq_suborder_all; dj. uf downward_subset; ap Z_inc. uh H7; ee; am. apply leq_trans with s. am. am. am. uf downward_subset; ap Z_inc. uh H7; ee; am. am. am. am. uf downward_subset; uhg; ir; Ztac. uf punctured_downward_subset; ap extensionality; uhg; ir; Ztac; ap Z_inc. ap H5; am. uh H10; uhg; xd. assert (leq a x1 x1). ap H7. ap leq_refl. am. am. uh H10; ee. apply leq_trans with y; am. uh H11; ee; am. uh H10; uhg; xd. rw H5. uh H2; ee. ap H6. ufi a H4; ufi downward_suborder H4; rwi underlying_suborder H4. ufi downward_subset H4; Ztac. Qed.
imports: Arith order