Skip to content
Snippets Groups Projects
Commit f106ebdd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add lemmas for 1/4 + 1/4.

parent b2f40d2a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 4 additions and 0 deletions
theories/numbers.v
+ 4
− 0
View file @ f106ebdd
...@@ -839,6 +839,8 @@ Lemma Qp_inv_1 : /1 = 1. ...@@ -839,6 +839,8 @@ Lemma Qp_inv_1 : /1 = 1.
Proof. apply (bool_decide_unpack _); by compute. Qed. Proof. apply (bool_decide_unpack _); by compute. Qed.
Lemma Qp_inv_half_half : /2 + /2 = 1. Lemma Qp_inv_half_half : /2 + /2 = 1.
Proof. apply (bool_decide_unpack _); by compute. Qed. 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. Lemma Qp_div_diag p : p / p = 1.
Proof. apply Qp_mul_inv_r. Qed. 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. ...@@ -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. 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. Lemma Qp_half_half : 1 / 2 + 1 / 2 = 1.
Proof. apply (bool_decide_unpack _); by compute. Qed. 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. Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1.
Proof. apply (bool_decide_unpack _); by compute. Qed. Proof. apply (bool_decide_unpack _); by compute. Qed.
Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1. Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment