Commit a8f65af5 authored by Robbert Krebbers's avatar Robbert Krebbers

Misc results about `Qp` fractions.

parent e29a5aee
......@@ -608,6 +608,12 @@ Lemma Qp_div_2 x : (x / 2 + x / 2 = x)%Qp.
Proof.
change 2%positive with (2 * 1)%positive. by rewrite Qp_div_S, Qp_div_1.
Qed.
Lemma Qp_half_half : (1 / 2 + 1 / 2 = 1)%Qp.
Proof. apply (bool_decide_unpack _); by compute. Qed.
Lemma Qp_quarter_three_quarter : (1 / 4 + 3 / 4 = 1)%Qp.
Proof. apply (bool_decide_unpack _); by compute. Qed.
Lemma Qp_three_quarter_quarter : (3 / 4 + 1 / 4 = 1)%Qp.
Proof. apply (bool_decide_unpack _); by compute. Qed.
Lemma Qp_lt_sum (x y : Qp) : (x < y)%Qc z, y = (x + z)%Qp.
Proof.
......
Markdown is supported
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