test-suite/success/NatRing.v


1
2
3
4
5
6
7
8
9
10

Require ArithRing.

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.