proposition: Lemma fintype_le1P : reflect (forall x : T, all_equal_to x) (#|T| <= 1).
proof: Proof. apply: (iffP (card_le1_eqP {:T})); [exact: in2T | exact: in2W]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)