proposition: Lemma fintype1P : reflect (exists x, all_equal_to x) (#|T| == 1).
proof: Proof. apply: (iffP idP) => [/eqP/fintype1|] [x eqx]; first by exists x. by apply/card1P; exists x => y; rewrite eqx !inE eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)