Created
June 14, 2016 12:41
-
-
Save gallais/8091c47f6bcc7486b5f50356169b3761 to your computer and use it in GitHub Desktop.
Various equivalences
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Reals. | |
| Open Scope R_scope. | |
| Goal forall x, x <> 0 -> 1 / x <> 0. | |
| intros. | |
| unfold Rdiv; rewrite Rmult_1_l. | |
| apply Rinv_neq_0_compat. | |
| assumption. | |
| Qed. | |
| Goal forall x, 1 / x = 0 -> x = 0. | |
| intros x H. | |
| destruct (Req_dec x 0); [assumption |]. | |
| rewrite <- (Rmult_1_l x), <- (Rinv_r x). | |
| unfold Rdiv in H; rewrite Rmult_1_l in H. | |
| rewrite H; ring. | |
| assumption. | |
| Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment