1 files changed, 8 insertions, 0 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index a461b26a0..50e0033e5 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -96,6 +96,14 @@ Ltac psatzl dom :=
 Ltac lra := 
   first [ psatzl R | psatzl Q ].
 
+Ltac nra := 
+  unfold Rdiv in * ; 
+  xnra ;     
+  abstract 
+    (intros __wit __varmap __ff ;
+     change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
+     apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
+                                                                       
 
 
 (* Local Variables: *)