diff options
| -rw-r--r-- | test-suite/success/NatRing.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/test-suite/success/NatRing.v b/test-suite/success/NatRing.v index 47d9f9b5a5..6a1eeccc6c 100644 --- a/test-suite/success/NatRing.v +++ b/test-suite/success/NatRing.v @@ -1,5 +1,10 @@ Require ArithRing. -Goal (S (S O))=(plus (S O) (S O)). +Lemma l1 : (S (S O))=(plus (S O) (S O)). NatRing. Qed. + +Lemma l2 : (x:nat)(S (S x))=(plus (S O) (S x)). +Intro. +NatRing. +Qed.
\ No newline at end of file |