proposition: Lemma ordinal_inc : forall o x:E, is_ordinal o -> inc x o = (leq_gen ID x o & x <> o).
proof: Proof. ir. ap iff_eq; ir. ee. wr ordinal_leq_leq_gen. uhg. ee; try am. apply ordinal_inc_ordinal with o; am. ap ordinal_inc_sub; am. uhg; ir. rwi H1 H0. apply ordinal_not_inc_itself with o; am. ee. wri ordinal_leq_leq_gen H0. uh H0. ee. ap ordinal_strict_sub_inc. am. am. uhg; ee; am. Qed.
imports: Arith transfinite