proposition: Lemma cardD1 x A : #|A| = (x \in A) + #|[predD1 A & x]|.
proof: Proof. case Ax: (x \in A); last first. by apply: eq_card => y /[!inE]/=; case: eqP => // ->. rewrite /= -(card1 x) -cardUI addnC /=. rewrite [#|predI _ _|]eq_card0 => [|y]; last by rewrite !inE; case: eqP. by apply: eq_card => y /[!inE]; case: eqP => // ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)