proposition: Lemma leq_gen_or : forall (f:E1) (x y:E), leq_gen f x x -> leq_gen f y y -> (leq_gen f x y \/ leq_gen f y x).
proof: Proof. ir. uh H; uh H0; nin H; nin H0; ee. cp (next_compatible_or H H0). nin H3. assert (inc x (U x1)). uh H3; ee. ap H5; uh H2; ee; am. assert (inc y (U x1)). uh H1; ee; am. rw (leq_gen_leq H0 H4 H5); rw (leq_gen_leq H0 H5 H4). uh H0; ee; uh H0; ee. uh H0; ee. ap H8; am. assert (inc y (U x0)). uh H3; ee. ap H5; uh H1; ee; am. assert (inc x (U x0)). uh H2; ee; am. rw (leq_gen_leq H H4 H5); rw (leq_gen_leq H H5 H4). uh H; ee; uh H; ee; uh H; ee. ap H8; am. Qed.
imports: Arith order