fact: Definition DC_ (X : Type) := forall R : X -> X -> Prop, (forall x, exists y, R x y) -> forall x, exists2 f, f 0 = x & path R f.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)