proposition: Lemma ordinal_strict_sub_inc : forall a o:E, is_ordinal a -> is_ordinal o -> strict_sub a o -> inc a o.
proof: Proof. ir. uh H; uh H0. cp H; cp H0. uh H; uh H0; nin H; nin H0. ee. assert (next x0 a= ID a). ap next_compatible_scale. am. apply leq_gen_scale_subset with ID. am. am. rw H0; uh H1; ee; am. rw H0; am. wr H0. ufi ID H6. wr H6. ap next_inc_U. rw H0; am. uh H4; ee; am. Qed.
imports: Arith transfinite