Skip to content
Snippets Groups Projects
Commit 3ce4e0e8 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 85aa6678 ad0c229d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 0 deletions
algebra/frac.v
+ 3
− 0
View file @ 3ce4e0e8
...@@ -35,3 +35,6 @@ Global Instance frac_full_exclusive : Exclusive 1%Qp. ...@@ -35,3 +35,6 @@ Global Instance frac_full_exclusive : Exclusive 1%Qp.
Proof. Proof.
move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
Qed. Qed.
Lemma frac_op': ∀ (p q: Qp), (p ⋅ q) = (p + q)%Qp.
Proof. done. Qed.
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