proposition: Lemma discrete_bool_compact : compact [set: discrete_topology discrete_bool].
proof: Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum interval rat) mathcomp(finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) reals signed topology HB(structures)