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