fact: Definition enumeration (A : Type) (u : nat -> A) (v : A -> nat) : Prop := (forall x : A, u (v x) = x) /\ (forall n : nat, v (u n) = n).
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon