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