I am trying to make a function like Definition cardinality (A : Ensemble U) : nat., so that for each ensemble I get its cardinal. I found this to be a challenging problem, and I would like to get some help.
By the way, there is cardinal U A n where if |A| = n then it becomes true.
One issue is that you cannot define this function for arbitrary sets: you need to assume that A is finite. You might use, for instance, the Finite predicate in Coq.Sets.Finite_sets. You might be tempted to use the finite_cardinal lemma from Coq.Sets.Finite_sets_facts, which says that every finite set has some cardinal. This would require you to extract a natural number out of an existence statement exists n, cardinal U A n, which in turn requires some form of the axiom of choice (e.g. choice in Coq.Logic.ClassicalChoice).