Commit 2019-09-03 09:24 94205c46

feat(data/fintype): prove card (subtype p) ≤ card α (#1383)

• feat(data/fintype): prove card (subtype p) ≤ card α
• Add cardinal.mk_le_of_subtype
• Rename mk_le_of_subtype to mk_subtype_le, use it in mk_set_le Earlier both mk_subtype_le and mk_set_le took set α as an argument. Now mk_subtype_le takes α → Prop.