From 3bf2e59b9231f8f2e42b5c3469b59230b56dd85a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 11 Sep 2017 12:01:53 -0400 Subject: fsatz tests: 1/(1/x) = x --- src/Algebra/Field_test.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/Algebra') 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. -- cgit v1.2.3