proposition: Lemma leq_gen_ordinal_leq : forall a o:E, leq_gen ID a o -> ordinal_leq a o.
proof: Proof. ir. uhg; dj. ap leq_gen_ordinal. apply leq_gen_def1 with o; am. ap leq_gen_ordinal; apply leq_gen_def2 with a; am. nin (leq_gen_is_next H). rw H2; uhg; ir; am. nin H2. ee. ap ordinal_inc_sub. am. ufi ID H4. rw H4; am. Qed.
imports: Arith transfinite