proposition: Lemma Rsth : Setoid_Theory R (@eq R).
proof: Proof. constructor;red;intros;subst;trivial. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain DiscrR ZArith Lia NsatzTactic Rbase Rfunctions RealField