diff --git a/theories/numbers.v b/theories/numbers.v
index 6d085fc0d92d2fcdc91058c0974d8ed3928fa10c..5f28384082982785c94bbd4aa020b6903b211742 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -839,6 +839,8 @@ Lemma Qp_inv_1 : /1 = 1.
 Proof. apply (bool_decide_unpack _); by compute. Qed.
 Lemma Qp_inv_half_half : /2 + /2 = 1.
 Proof. apply (bool_decide_unpack _); by compute. Qed.
+Lemma Qp_inv_quarter_quarter : /4 + /4 = /2.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
 
 Lemma Qp_div_diag p : p / p = 1.
 Proof. apply Qp_mul_inv_r. Qed.
@@ -868,6 +870,8 @@ Lemma Qp_div_S p q : p / (2 * q) + p / (2 * q) = p / q.
 Proof. by rewrite <-Qp_div_add_distr, Qp_add_diag, Qp_div_mul_cancel_l. Qed.
 Lemma Qp_half_half : 1 / 2 + 1 / 2 = 1.
 Proof. apply (bool_decide_unpack _); by compute. Qed.
+Lemma Qp_quarter_quarter : 1 / 4 + 1 / 4 = 1 / 2.
+Proof. apply (bool_decide_unpack _); by compute. Qed.
 Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1.
 Proof. apply (bool_decide_unpack _); by compute. Qed.
 Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1.