proposition: Lemma leq_gen_bottom_elt : forall (f:E1)(y:E), (forall x:E, inc x y -> leq_gen f x x) -> nonempty y -> exists b:E, (inc b y & (forall x:E, inc x y -> leq_gen f b x)).
proof: Proof. ir. nin H0. cp (H _ H0). uh H1; nin H1; ee. pose (w:=(intersection2 y (U x))). cp H1. uh H3; ee. uh H3; ee. assert (nonempty w). sh y0. uf w. ap intersection2_inc. am. uh H2; ee; am. assert (sub w (U x)). uf w. uhg; ir. cp (intersection2_second H7). am. cp (H5 _ H7 H6). nin H8. sh x0. ee. uh H8. ee. ufi w H9. cp (intersection2_first H9). am. ir. rw leq_gen_char; ee. assert (leq_gen f x1 x1). ap H; am. uh H10; nin H10; ee. sh (U x2). ee. uhg. sh x2; ee. tv. am. uh H11; ee; am. ir. uh H10; nin H10; ee. cp (next_compatible_or H1 H12). nin H13. uh H13; ee. wr H10. ap H15. ap H7. uh H8; ee. am. assert (scale_subset w0 x). wr H10. apply next_comp_sub_scale with f. am. am. uh H13; ee; am. uh H14; ee. apply H16 with x1. am. uh H8. ee. uh H8; ee. apply H20. uf w; ap intersection2_inc. am. ap H15. am. Qed.
imports: Arith order