Commit 03ad1620 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Added opp_Z2R.

parent d8afcec3
......@@ -79,6 +79,14 @@ apply Ropp_eq_compat.
apply P2R_INR.
Qed.
Lemma opp_Z2R :
forall n, Z2R (-n) = (- Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply Ropp_Ropp_IZR.
Qed.
Lemma plus_Z2R :
forall m n, (Z2R (m + n) = Z2R m + Z2R n)%R.
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