fact: Definition quotient_projection (x:A) : quotient := exist _ (equiv_class x) (equiv_class_in_quotient x).
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec