proposition: Lemma ordinal_lt_rw : forall a o:E, ordinal_lt a o = (is_ordinal o&inc a o).
proof: Proof. ir. uf ordinal_lt. uf ordinal_leq; ap iff_eq; ir; xd. rw ordinal_inc_rw. uf strict_sub; xd. am. rwi ordinal_inc_rw H0; ee; am. rwi ordinal_inc_rw H0; ee. uh H1; ee; am. am. rwi ordinal_inc_rw H0; ee. uh H1; ee; am. am. Qed.
imports: Arith transfinite