proposition: Lemma Neqe : ring_eq_ext N.add N.mul Nopp (@eq N).
proof: Proof. Proof (SReqe_Reqe Nseqe). Lemma Nath : almost_ring_theory 0%N 1%N N.add N.mul Nsub Nopp (@eq N). Proof (SRth_ARth Nsth Nth). Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y. Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom