proposition: Lemma quotient_continuous {Z : topologicalType} (f : Q -> Z) : continuous f <-> continuous (f \o \pi_Q).
proof: Proof. split => /continuousP /= cts; apply/continuousP => A oA; last exact: cts. by rewrite comp_preimage; move/continuousP: pi_continuous; apply; exact: cts. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed