proposition: Lemma card_le1P {A} : reflect {in A, forall x, A =i pred1 x} (#|A| <= 1).
proof: Proof. apply: (iffP idP) => [A1 x xA y|]; last first. by have [/= x xA /(_ _ xA)/eq_card1->|/eq_card0->//] := pickP [in A]. move: A1; rewrite (cardD1 x) xA ltnS leqn0 => /eqP/card0_eq/(_ y). by rewrite !inE; have [->|]:= eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)