NatRing.v « success « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/success/NatRing.v

blob: 22d021d543008d664999d6ba3c0bc3b850d52732 (plain)

Require Import ArithRing.

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

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