diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-09-11 12:01:53 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-09-11 12:02:02 -0400 |
| commit | 3bf2e59b9231f8f2e42b5c3469b59230b56dd85a (patch) | |
| tree | 135b75a852a8c65d90ccf7205fc60df33ecce0de /src/Algebra | |
| parent | b87cd7cb1d6f704807f12e0a259b910e6b7ee2c0 (diff) | |
fsatz tests: 1/(1/x) = x
Diffstat (limited to 'src/Algebra')
| -rw-r--r-- | src/Algebra/Field_test.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v index 149a6373e..3bdd65089 100644 --- a/src/Algebra/Field_test.v +++ b/src/Algebra/Field_test.v @@ -24,6 +24,9 @@ Module _fsatz_test. Lemma div_goal a b c d (H:a=b+c) (anz:a<>0) : d/a + 1 = (d+b+c)/(b+c). Proof using Type*. fsatz. Qed. + Lemma inv_inv x (H:x <> 0) : 1/(1/x) = x. + Proof using Type*. fsatz. Qed. + Lemma zero_neq_one : 0 <> 1. Proof using Type*. fsatz. Qed. |