`{PropResizing} `{Univalence} (B C : Ordinal) : B < C -> card B ≤ card C. Proof. intros B_C. apply tr. cbn. rewrite (bound_property B_C). exists out. apply isinjective_simulation. apply is_simulation_out. Qed.
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra HSet. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Card. From HoTT.Sets Require Import Ordinals Powers.