proposition: Lemma leq_gen_trans : forall (f:E1)(x y z:E), leq_gen f x y -> leq_gen f y z -> leq_gen f x z.
proof: Proof. ir. cp H. cp H0. uh H; uh H0. nin H; nin H0. ee. cp (next_compatible_or H H0). nin H5. uh H5. ee. assert (inc x (U x1)). ap H7. uh H4; ee; am. assert (inc y (U x1)). uh H3; ee; am. assert (inc z (U x1)). uh H3; ee; am. cp (leq_gen_leq H0 H9 H10). cp (leq_gen_leq H0 H10 H11). cp (leq_gen_leq H0 H9 H11). rw H14. apply leq_trans with y. am. wr H12; am. am. uh H5; ee. assert (inc x (U x0)). uh H4; ee; am. assert (inc y (U x0)). uh H4; ee; am. assert (inc z (U x0)). ap H7; uh H3; ee; am. cp (leq_gen_leq H H9 H10). cp (leq_gen_leq H H9 H11). cp (leq_gen_leq H H10 H11). rw H13. apply leq_trans with y. am. am. wr H14; am. Qed.
imports: Arith order