proposition: Lemma fintype1 : #|T| = 1 -> {x : T | all_equal_to x}.
proof: Proof. by move=> /mem_card1[x ex]; exists x => y; suff: y \in T by rewrite ex => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)