Lemma fsubsetU1 x A : A `<=` x |` A.
Lemma fset1U1 x B : x \in x |` B.
Lemma fsetU1l x A b : x \in A -> x \in A `|` [fset b].
Lemma fsetU11 x B : x \in x |` B.
Lemma fsetU1r A b : b \in A `|` [fset b].
Lemma fsetU1K a B : a \notin B -> (a |` B) `\ a = B.
Lemma cardfsU1 a A : #|` a |` A| = (a \notin A) + #|` A|.
Lemma fdisjointU1X x A B :
    [disjoint x |` A & B]%fset = (x \notin B) && [disjoint A & B]%fset.
Lemma imfsetU1 f a A : f @` (a |` A) = f a |` (f @` A).
Lemma big_fsetU1 (a : I) (A : {fset I}) (F : I -> R) : a \notin A ->
    \big[op/idx]_(i <- (a |` A)) F i = op (F a) (\big[op/idx]_(i <- A) F i).

Lemma msetU1l x A B : x \in A -> x \in A `|` B.
Lemma msetU1r A b : b \in A `|` [mset b].
Lemma msetU1K a B : a \notin B -> (a |` B) `\ a = B.
Lemma mset1U1 x B : x \in x |` B. Proof. by rewrite !inE eqxx. Qed.
Lemma msubsetU1 x A : A `<=` (x |` A).

Lemma in_fset1U a' A a : (a \in a' |` A) = (a == a') || (a \in A).
Lemma fset1UP x a B : reflect (x = a \/ x \in B) (x \in a |` B).
Lemma fset1U1 x B : x \in x |` B. Proof. by rewrite !inE eqxx. Qed.
Lemma fset1Ur x a B : x \in B -> x \in a |` B.
Lemma fset21 a b : a \in [fset a; b]. Proof. by rewrite fset1U1. Qed.
Lemma mem_fset1U a A : a \in A -> a |` A = A.
Lemma fset1U_rect (T : choiceType) (P : {fset T} -> Type) :
  P fset0 ->
  (forall x X, x \notin X -> P X -> P (x |` X)) ->
  forall X, P X.

Lemma mset1UE a A b : (a |` A) b = maxn (b == a) (A b).
Lemma in_mset1U a' A a : (a \in a' |` A) = (a == a') || (a \in A).
Lemma mset1U1 x B : x \in x |` B. Proof. by rewrite !inE eqxx. Qed.
Lemma mset1Ur x a B : x \in B -> x \in a |` B.
Lemma mset1UP x a B : reflect (x = a \/ x \in B) (x \in a |` B).
Lemma mem_mset1U a A : a \in A -> a |` A = A.