proposition: Lemma sow_smallest : forall (p:EP) o, is_ordinal o -> p o -> ordinal_leq (sow p) o.
proof: Proof. ir. cp (sow_is_sow p). uh H1; ee. util H2. sh o; ee; am. uh H3; ee. cp (H5 _ H H0). uhg; ee. ap sow_ordinal. am. am. Qed.
imports: Arith transfinite