aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/NatRing.v
blob: 8426c7e482fd6052fe16d2e6ba6cd9af3dbabbc3 (plain)
1
2
3
4
5
6
7
8
9
10
Require Import ArithRing.

Lemma l1 : 2 = 1 + 1.
ring_nat.
Qed.

Lemma l2 : forall x : nat, S (S x) = 1 + S x.
intro.
ring_nat.
Qed.