Library Coq.ring.LegacyNArithRing




Require Import Bool.
Require Export LegacyRing.
Require Export ZArith_base.
Require Import NArith.
Require Import Eqdep_dec.


Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m.

Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq.
Qed.

Add Legacy Semi Ring
  N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].