proposition: Lemma card1P A : reflect (exists x, A =i pred1 x) (#|A| == 1).
proof: Proof. by apply: (iffP idP) => [/eqP/mem_card1[x inA]|[x /eq_card1/eqP//]]; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)