proposition: Lemma set1_inj : injective (@set1 T).
proof: Proof. by move=> a b eqsab; apply/set1P; rewrite -eqsab set11. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)