diff options
Diffstat (limited to 'src/Galois/GaloisExamples.v')
| -rw-r--r-- | src/Galois/GaloisExamples.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v index f649701b7..12bcfa2c8 100644 --- a/src/Galois/GaloisExamples.v +++ b/src/Galois/GaloisExamples.v @@ -42,6 +42,12 @@ Module Example31. field; trivial. Qed. + Lemma example4: forall x: GF, x/(inject 1) = x. + Proof. + intros; field. + discriminate. + Qed. + End Example31. Module TimesZeroTransparentTestModule. |