proposition: Lemma indic_fimfun_subproof X : @FiniteImage aT rT \1_X.
proof: Proof. split; apply: (finite_subfset [fset 0; 1]%fset) => x [tt /=]. by rewrite !inE indicE; case: (_ \in _) => _ <-; rewrite ?eqxx ?orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets fsbigop) mathcomp(functions cardinality set_interval) signed reals ereal topology normedtype sequences