proposition: Lemma mem_card1 A : #|A| = 1 -> {x | A =i pred1 x}.
proof: Proof. move=> A1; have /card_gt0P/sigW[x xA]: #|A| > 0 by rewrite A1. by exists x; apply/card_le1P; rewrite ?A1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)