proposition: Lemma leq_gen_char : forall (f:E1)(x y:E), leq_gen f x y = ((exists w:E, (is_leq_gen_scale f w & inc y w))& (forall w:E, is_leq_gen_scale f w -> inc y w -> inc x w)).
proof: Proof. ir. ap iff_eq; ir. ee. uh H; nin H; ee. sh (U x0). ee. ap next_comp_leq_gen_scale. am. uh H0; ee; am. ir. uh H; nin H; ee. assert (is_leq_gen_scale f (U x0)). ap next_comp_leq_gen_scale. am. cp (leq_gen_scale_or H0 H3). nin H4. cp (leq_gen_scale_subset H H0 H4). uh H5; ee. apply H7 with y. am. am. ap H4. uh H2; ee; am. ee. nin H. ee. uh H; nin H; ee. pose (u := punctured_downward_subset x1 y). assert (scale_subset u x1). uf u. ap punctured_downward_scale. uh H2; ee; am. rw H; am. assert (next x1 u = y). uf u. sy; ap next_punctured_downward. uh H2; ee; am. rw H; am. pose (v:=tack_on u y). assert (scale_subset v x1). uf v. wr H4. ap scale_subset_next. am. uhg; ee. uhg; uhg; ir. assert (inc y u). rw H5; rw H; am. ufi u H6; ufi punctured_downward_subset H6; Ztac. uh H8; ee. ap H9; tv. uh H3; ee; am. assert (inc x v). ap H0. apply scale_subset_is_leq_gen_scale with x1. am. am. uf v. rw tack_on_inc. ap or_intror; tv. ufi v H6. rwi tack_on_inc H6. nin H6. ufi u H6; ufi punctured_downward_subset H6; Ztac. assert (leq x1 x y = leq_gen f x y). sy. ap leq_gen_leq. am. am. rw H; am. wr H9. uh H8; ee; am. rw H6. uhg; ee. sh x1; ee; try am. ap leq_refl. uh H2; ee; uh H2; ee; uh H2; ee; am. rw H; am. Qed.
imports: Arith order