Theorem Cardinal.mk_subtype_le

Modification history