Commit b150be40 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Added eq/neq_Z2R.

parent 6d7a279c
......@@ -229,6 +229,22 @@ now apply le_Z2R.
now apply lt_Z2R.
Qed.
Lemma eq_Z2R :
forall m n, (Z2R m = Z2R n)%R -> (m = n)%Z.
Proof.
intros m n H.
apply eq_IZR.
now rewrite <- 2!Z2R_IZR.
Qed.
Lemma neq_Z2R :
forall m n, (Z2R m <> Z2R n)%R -> (m <> n)%Z.
Proof.
intros m n H H'.
apply H.
now apply f_equal.
Qed.
Lemma Z2R_neq :
forall m n, (m <> n)%Z -> (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