From f106ebdd476c0372b02f621f69188877e825a33c Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 7 Oct 2020 10:40:04 +0200 Subject: [PATCH] Add lemmas for 1/4 + 1/4. --- theories/numbers.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/theories/numbers.v b/theories/numbers.v index 6d085fc0..5f283840 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. -- GitLab