Missing lemmas about Prop: absorbing or neutral elements for various operations

I asked the question on zulip, but didn't get much feedback. At first I didn't find anything to rewrite True /\ P to P, but then I realized there might be other similar situations ; here is some code:

Require Import Setoid. (* FIXME: why!? *)
 
Section Missing.

Variable P: Prop.

Lemma and_true_l: True /\ P <-> P.
Proof.
split.
  intros [_ ?].
  assumption.
intros ?.
split.
  exact I.
assumption.
Qed.

Lemma and_true_r: P /\ True <-> P.
Proof.
rewrite and_comm.
exact and_true_l.
Qed.

Lemma and_false_l: False /\ P <-> False.
Proof.
split.
  intros [? _].
  assumption.
intros ?.
exfalso.
assumption.
Qed.

Lemma and_false_r: P /\ False <-> False.
Proof.
rewrite and_comm.
exact and_false_l.
Qed.

Lemma or_true_l: True \/ P <-> True.
Proof.
split.
  intros _.
  exact I.
intros ?.
left.
assumption.
Qed.

Lemma or_true_r: P \/ True <-> True.
Proof.
rewrite or_comm.
exact or_true_l.
Qed.

Lemma or_false_l: False \/ P <-> P.
Proof.
split.
  intro H.
  case H.
    intros ?.
    exfalso ; assumption.
  intros ?.
  assumption.
intros ?.
right.
assumption.
Qed.

Lemma or_false_r: P \/ False <-> P.
Proof.
rewrite or_comm.
exact or_false_l.
Qed.

Lemma impl_false_l: (False -> P) <-> True.
Proof.
split.
  intros _.
  exact I.
intros _ ?.
exfalso ; assumption.
Qed.

Lemma impl_true_l: (True -> P) <-> P.
Proof.
split.
  intro H.
  exact (H I).
intros ? _.
assumption.
Qed.

Lemma impl_true_r: (P -> True) <-> True.
Proof.
split.
  intros _.
  exact I.
intros _ _.
exact I.
Qed.

End Missing.

(Notice: I'm more used to writing proof in MC-style, so my proofs in pure Coq might be a bit awkward...)

They are supposed to be used for rewriting complex goals (which is why the existing False_ind and my impl_false_l might both make sense).

Start by locating the existing standard-library lemmas for Prop and the file where related rewriting lemmas are defined. Compare the requested lemmas and their intended rewriting behavior with the existing API; done means the agreed absorbing and neutral-element lemmas are added with suitable coverage.