Skip to content

Commit

Permalink
One more lemma from Cezary.
Browse files Browse the repository at this point in the history
git-archimport-id: r.oconnor@cs.ru.nl--Nijmegen/CoRN--coq-trunk--0--patch-37
Russell O'Connor committed Jul 9, 2008
1 parent 4ed9c7a commit 801558b
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions coq_reals/Rreals_iso.v
Original file line number Diff line number Diff line change
@@ -77,6 +77,13 @@ Qed.

(** apartness *)

Lemma R_eq_as_IR_back : forall x y, (RasIR x [=] RasIR y -> x = y).
intros x y H.
replace x with (IRasR (RasIR x)) by apply RasIRasR_id.
replace y with (IRasR (RasIR y)) by apply RasIRasR_id.
rapply map_wd_unfolded; assumption.
Qed.

Lemma R_ap_as_IR : forall x y, (RasIR x [#] RasIR y -> x <> y).
intros x y H.
replace x with (IRasR (RasIR x)) by apply RasIRasR_id.

0 comments on commit 801558b

Please sign in to comment.