Commit ad0c229d authored by Zhen Zhang's avatar Zhen Zhang

Add rewrite lemma for frac_op

parent f4b671c8
Pipeline #2801 passed with stage
in 9 minutes and 21 seconds
......@@ -35,3 +35,6 @@ Global Instance frac_full_exclusive : Exclusive 1%Qp.
Proof.
move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
Qed.
Lemma frac_op': (p q: Qp), (p q) = (p + q)%Qp.
Proof. done. Qed.
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