proposition: Lemma set_mem {T : finType} (s : {set T}) : s = finset (ssrbool.mem (enum s)).
proof: Proof. apply/setP=> i. by rewrite !inE mem_enum. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR f2