proposition: Lemma leq_gen_scale_tack_on : forall (f:E1)(y:E), is_leq_gen_scale f y -> ~inc (f y) y -> is_leq_gen_scale f (tack_on y (f y)).
proof: Proof. ir. uh H; nin H; ee. assert (forall u v:E, inc u y-> inc v y-> leq x u v = leq_gen f u v). ir; sy; ap leq_gen_leq; try am. rw H; am. rw H; am. uhg. pose (a:= create (tack_on (U x) (f y)) (new_order x (f y))). sh a; dj. uf a; rw underlying_create. rw H; tv. assert (forall u v:E, inc u (U a) -> inc v (U a) -> leq a u v = new_order x (f y) u v). ir. uf a. rw leq_create. tv. rw H; wr H3; am. rw H; wr H3; am. uhg; dj. uf a. ap new_order_wo. rw H; am. uh H1; ee; am. rwi H3 H6. rwi tack_on_inc H6; nin H6. assert (punctured_downward_subset a y0 = punctured_downward_subset x y0). ap extensionality; uhg. intro. do 2 (rw inc_punctured_downward_subset); ir. xd. rw H. rwi H3 H7; rwi tack_on_inc H7; nin H7. am. rwi H4 H8. uh H8. nin H8. wr H. uh H8; ee; am. rw H7; wr H8; am. uh H8; ee; am. uh H8; ee; am. rwi H4 H8; uh H8; nin H8. am. assert False. ap H0. wr H8; am. elim H10. ee. am. ee; am. intro. do 2 (rw inc_punctured_downward_subset); ir. xd. rw H3; rw tack_on_inc; ap or_introl; rwi H H7; am. assert (sub (U x) (U a)). rw H; uhg; ir; rw H3; rw tack_on_inc; ap or_introl; am. rw H4. uhg. ap or_introl; am. ap H10; am. ap H10; rw H; am. rw H7. uh H1; ee. ap H8. rw H; am. transitivity (f y); try (sy; am). assert (punctured_downward_subset a y0 = y). ap extensionality; uhg; intro; rw inc_punctured_downward_subset; ir. ee. rwi H3 H7; rwi tack_on_inc H7; nin H7. am. assert False. ap H9; rw H6; rw H7; tv. elim H10. dj. rw H3; rw tack_on_inc; ap or_introl; am. rw H4. uhg. ap or_intror; am. am. rw H6. rw H3; rw tack_on_inc. ap or_intror; tv. uhg; ir. ap H0. wr H6; wr H10. am. rw H7; tv. Qed.
imports: Arith order