[micromega] fix efficiency regression

PR #9725 fixes completness bugs introduces some inefficiency. The
current PR intends to fix the inefficiency while retaining
completness. The fix removes a pre-processing step and instead relies
on a more elaborate proof format introducing positivity constraints on
the fly.

Solve bootstrapping issues: RMicromega <-> Rbase <-> lia.

Fixes #11063 and fixes #11242 and fixes #11270

29 files changed, 965 insertions, 813 deletions

diff --git a/doc/changelog/04-tactics/11263-micromega-fix.rst b/doc/changelog/04-tactics/11263-micromega-fix.rst
new file mode 100644
index 0000000000..ebfb6c19b1
--- /dev/null
+++ b/doc/changelog/04-tactics/11263-micromega-fix.rst
@@ -0,0 +1,6 @@
+- **Fixed**
+  Efficiency regression introduced by  PR `#9725 <https://github.com/coq/coq/pull/9725>`_.
+  (`#11263 <https://github.com/coq/coq/pull/11263>`_,
+  fixes `#11063 <https://github.com/coq/coq/issues/11063>`_,
+  and `#11242 <https://github.com/coq/coq/issues/11242>`_,
+  and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson).
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index a2bc90ffc0..b816ef6210 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -24,6 +24,7 @@ plugins/extraction/Extraction.v
 plugins/funind/FunInd.v
 plugins/funind/Recdef.v
 plugins/ltac/Ltac.v
+plugins/micromega/Ztac.v
 plugins/micromega/DeclConstant.v
 plugins/micromega/Env.v
 plugins/micromega/EnvRing.v
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 55a93eade7..e53800d07d 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -23,28 +23,13 @@ Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
 
-Ltac zchange checker :=
+Ltac zchecker :=
   intros __wit __varmap __ff ;
-  change (@Tauto.eval_bf _ (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-  apply (checker __ff __wit).
-
-Ltac zchecker_no_abstract checker :=
-  zchange checker ; vm_compute ; reflexivity.
-
-Ltac zchecker_abstract checker :=
-  abstract (zchange checker ; vm_cast_no_check (eq_refl true)).
-
-Ltac zchecker := zchecker_no_abstract ZTautoChecker_sound.
-
-(*Ltac zchecker_ext := zchecker_no_abstract ZTautoCheckerExt_sound.*)
-
-Ltac zchecker_ext :=
-  intros __wit __varmap __ff ;
-  exact (ZTautoCheckerExt_sound __ff __wit
-                                (@eq_refl bool true <: @eq bool (ZTautoCheckerExt __ff __wit) true)
+  exact (ZTautoChecker_sound __ff __wit
+                                (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true)
                                 (@find Z Z0 __varmap)).
 
-Ltac lia := PreOmega.zify; xlia zchecker_ext.
+Ltac lia := PreOmega.zify; xlia zchecker.
                
 Ltac nia := PreOmega.zify; xnlia zchecker.
 
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 80e0f3a536..0e8c09ef1b 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -56,7 +56,7 @@ Extract Constant Rinv   => "fun x -> 1 / x".
 (*Extraction "micromega.ml"
            Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
            Tauto.abst_form
-           ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ
+           ZMicromega.cnfZ  ZMicromega.Zeval_const QMicromega.cnfQ
            List.map simpl_cone (*map_cone  indexes*)
            denorm Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 6c1852acbf..0f7a02c2c9 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -17,12 +17,12 @@
 Require Import OrderedRing.
 Require Import RingMicromega.
 Require Import Refl.
-Require Import Raxioms Rfunctions RIneq Rpow_def DiscrR.
+Require Import Raxioms Rfunctions RIneq Rpow_def.
 Require Import QArith.
 Require Import Qfield.
 Require Import Qreals.
 Require Import DeclConstant.
-Require Import Lia.
+Require Import Ztac.
 
 Require Setoid.
 (*Declare ML Module "micromega_plugin".*)
@@ -334,15 +334,16 @@ Proof.
       apply Qeq_bool_eq in C2.
       rewrite C2.
       simpl.
-      rewrite Qpower0 by lia.
+      rewrite Qpower0.
       apply Q2R_0.
+      intro ; subst ; slia C1 C1.
     + rewrite Q2RpowerRZ.
       rewrite IHc.
       reflexivity.
       rewrite andb_false_iff in C.
       destruct C.
       simpl. apply Z.ltb_ge in H.
-      lia.
+      right ; normZ. slia H H0.
       left ; apply Qeq_bool_neq; auto.
     + simpl.
       rewrite <- IHc.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index c1edf579cf..aa8876357a 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -856,7 +856,7 @@ Proof.
       simpl.
       tauto.
     +
-      rewrite <- eval_cnf_cons_iff with (1:= fun env (term:Formula Z) => True) .
+      rewrite <- eval_cnf_cons_iff.
       simpl.
       unfold eval_tt. simpl.
       rewrite IHl.
@@ -940,7 +940,7 @@ Proof.
   destruct (check_inconsistent f) eqn:U.
   - destruct f as [e op].
     assert (US := check_inconsistent_sound _ _ U env).
-    rewrite eval_cnf_ff with (1:= eval_nformula).
+    rewrite eval_cnf_ff.
     tauto.
   - intros. rewrite cnf_of_list_correct.
     now apply xnormalise_correct.
@@ -956,7 +956,7 @@ Proof.
   -
     destruct f as [e o].
     assert (US := check_inconsistent_sound _  _ U env).
-    rewrite eval_cnf_tt with (1:= eval_nformula).
+    rewrite eval_cnf_tt.
     tauto.
   - rewrite cnf_of_list_correct.
     apply xnegate_correct.
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 02dd29ef14..a155207e2e 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -938,8 +938,6 @@ Section S.
       Qed.
 
 
-    Variable eval  : Env -> Term -> Prop.
-
     Variable eval'  : Env -> Term' -> Prop.
 
     Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d).
@@ -1202,7 +1200,7 @@ Section S.
   Qed.
 
 
-
+  Variable eval  : Env -> Term -> Prop.
 
   Variable normalise_correct : forall env t tg, eval_cnf  env (normalise t tg) -> eval env t.
 
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index d709fdda14..9bedb47371 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -18,11 +18,11 @@ Require Import List.
 Require Import Bool.
 Require Import OrderedRing.
 Require Import RingMicromega.
-Require  FSetPositive FSetEqProperties.
 Require Import ZCoeff.
 Require Import Refl.
 Require Import ZArith_base.
 Require Import ZArithRing.
+Require Import Ztac.
 Require PreOmega.
 (*Declare ML Module "micromega_plugin".*)
 Local Open Scope Z_scope.
@@ -30,7 +30,7 @@ Local Open Scope Z_scope.
 Ltac flatten_bool :=
   repeat match goal with
            [ id : (_ && _)%bool = true |- _ ] =>  destruct (andb_prop _ _ id); clear id
-           |  [ id : (_ || _)%bool = true |- _ ] =>  destruct (orb_prop _ _ id); clear id
+         |  [ id : (_ || _)%bool = true |- _ ] =>  destruct (orb_prop _ _ id); clear id
          end.
 
 Ltac inv H := inversion H ; try subst ; clear H.
@@ -186,6 +186,7 @@ match o with
 | OpGt => Z.gt
 end.
 
+
 Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):=
   let (lhs, op, rhs) := f in
     (Zeval_op2 op) (Zeval_expr env lhs) (Zeval_expr env rhs).
@@ -193,10 +194,13 @@ Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):=
 Definition Zeval_formula' :=
   eval_formula  Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt (fun x => x) (fun x => x) (pow_N 1 Z.mul).
 
-Lemma Zeval_formula_compat : forall env f, Zeval_formula env f <-> Zeval_formula' env f.
+Lemma Zeval_formula_compat' : forall env f,  Zeval_formula env  f <-> Zeval_formula' env f.
 Proof.
-  destruct f ; simpl.
-  rewrite Zeval_expr_compat. rewrite Zeval_expr_compat.
+  intros.
+  unfold Zeval_formula.
+  destruct f.
+  repeat rewrite Zeval_expr_compat.
+  unfold Zeval_formula' ; simpl.
   unfold eval_expr.
   generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
         (fun x : N => x) (pow_N 1 Z.mul) env Flhs).
@@ -308,10 +312,10 @@ Definition xnnormalise (t : Formula Z) : NFormula Z :=
 
 Lemma xnnormalise_correct :
   forall env f,
-    eval_nformula env (xnnormalise f) <-> Zeval_formula env f.
+    eval_nformula env (xnnormalise f) <-> Zeval_formula env  f.
 Proof.
   intros.
-  rewrite Zeval_formula_compat.
+  rewrite Zeval_formula_compat'.
   unfold xnnormalise.
   destruct f as [lhs o rhs].
   destruct o eqn:O ; cbn ; rewrite ?eval_pol_sub;
@@ -418,7 +422,7 @@ Proof.
       specialize (Zunsat_sound _ EQ env).
       tauto.
     +
-      rewrite <- eval_cnf_cons_iff with (1:= fun env (term:Formula Z) => True) .
+      rewrite <- eval_cnf_cons_iff.
       rewrite IHf.
       simpl.
       unfold E at 2.
@@ -439,7 +443,7 @@ Proof.
   generalize (xnnormalise t) as f;intro.
   destruct (Zunsat f) eqn:U.
   - assert (US := Zunsat_sound _  U env).
-    rewrite eval_cnf_ff with (1:= eval_nformula).
+    rewrite eval_cnf_ff.
     tauto.
   - rewrite cnf_of_list_correct.
     apply xnormalise_correct.
@@ -474,7 +478,7 @@ Proof.
   - tauto.
 Qed.
 
-Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env t.
+Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env  t.
 Proof.
   intros.
   rewrite <- xnnormalise_correct.
@@ -482,13 +486,13 @@ Proof.
   generalize (xnnormalise t) as f;intro.
   destruct (Zunsat f) eqn:U.
   - assert (US := Zunsat_sound _  U env).
-    rewrite eval_cnf_tt with (1:= eval_nformula).
+    rewrite eval_cnf_tt.
     tauto.
   - rewrite cnf_of_list_correct.
     apply xnegate_correct.
 Qed.
 
-Definition cnfZ (Annot TX AF : Type) (f : TFormula (Formula Z) Annot TX AF) :=
+Definition cnfZ (Annot: Type) (TX : Type)  (AF : Type)  (f : TFormula (Formula Z) Annot TX AF) :=
   rxcnf Zunsat Zdeduce normalise negate true f.
 
 Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool :=
@@ -555,7 +559,8 @@ Inductive ZArithProof :=
 | RatProof : ZWitness -> ZArithProof -> ZArithProof
 | CutProof : ZWitness -> ZArithProof -> ZArithProof
 | EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof
-(*| ExProof   : positive -> positive -> positive -> ZArithProof  ExProof z t x : exists z t, x = z - t /\ z >= 0 /\ t >= 0 *)
+| ExProof   : positive -> ZArithProof -> ZArithProof
+(*ExProof x : exists z t, x = z - t /\ z >= 0 /\ t >= 0 *)
 .
 (*| SplitProof :   PolC Z -> ZArithProof -> ZArithProof -> ZArithProof.*)
 
@@ -826,187 +831,171 @@ Definition valid_cut_sign (op:Op1) :=
     | _         => false
   end.
 
-Module Vars.
-  Import FSetPositive.
-  Include PositiveSet.
 
-  Module Facts := FSetEqProperties.EqProperties(PositiveSet).
+Definition bound_var (v : positive) : Formula Z :=
+  Build_Formula (PEX v) OpGe (PEc 0).
 
-  Lemma mem_union_l : forall x s s',
-      mem x s = true ->
-      mem x (union s s') = true.
-  Proof.
-    intros.
-    rewrite Facts.union_mem.
-    rewrite H. reflexivity.
-  Qed.
+Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z :=
+  Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)).
 
-  Lemma mem_union_r : forall x s s',
-      mem x s' = true ->
-      mem x (union s s') = true.
-  Proof.
-    intros.
-    rewrite Facts.union_mem.
-    rewrite H. rewrite orb_comm. reflexivity.
-  Qed.
 
-  Lemma mem_singleton : forall p,
-      mem p (singleton p) = true.
-  Proof.
-    apply Facts.singleton_mem_1.
-  Qed.
+Fixpoint vars (jmp : positive) (p : Pol Z) : list positive :=
+  match p with
+  | Pc c => nil
+  | Pinj j p => vars (Pos.add j jmp) p
+  | PX p j q => jmp::(vars jmp p)++vars (Pos.succ jmp) q
+  end.
 
-  Lemma mem_elements : forall x v,
-      mem x v = true <-> List.In x (PositiveSet.elements v).
-  Proof.
-    intros.
-    rewrite Facts.MP.FM.elements_b.
-    rewrite existsb_exists.
-    unfold Facts.MP.FM.eqb.
-    split ; intros.
-    - destruct H as (x' & IN & EQ).
-    destruct (PositiveSet.E.eq_dec x x') ; try congruence.
-    subst ; auto.
-    - exists x.
-      split ; auto.
-      destruct (PositiveSet.E.eq_dec x x) ; congruence.
-  Qed.
+Fixpoint max_var (jmp : positive) (p : Pol Z) : positive :=
+  match p with
+  | Pc _ => jmp
+  | Pinj j p => max_var (Pos.add j jmp) p
+  | PX p j q => Pos.max (max_var jmp p) (max_var (Pos.succ jmp) q)
+  end.
 
-  Definition max_element (vars : t)  :=
-    fold Pos.max vars xH.
+Lemma pos_le_add : forall y x,
+    (x <= y + x)%positive.
+Proof.
+  intros.
+  assert  ((Z.pos x) <= Z.pos (x + y))%Z.
+  rewrite <- (Z.add_0_r (Zpos x)).
+  rewrite <- Pos2Z.add_pos_pos.
+  apply Z.add_le_mono_l.
+  compute. congruence.
+  rewrite Pos.add_comm in H.
+  apply H.
+Qed.
 
-  Lemma max_element_max :
-    forall x vars, mem x vars = true -> Pos.le x (max_element vars).
-  Proof.
-    unfold max_element.
-    intros.
-    rewrite mem_elements in H.
-    rewrite PositiveSet.fold_1.
-    set (F := (fun (a : positive) (e : PositiveSet.elt) => Pos.max e a)).
-    revert H.
-    assert  (((x <= 1 -> x <= fold_left F (PositiveSet.elements vars) 1)
-             /\
-            (List.In x (PositiveSet.elements vars) ->
-             x <= fold_left F (PositiveSet.elements vars) 1))%positive).
-    {
-    revert x.
-    generalize xH as acc.
-    induction (PositiveSet.elements  vars).
-    - simpl. tauto.
-    - simpl.
-      intros.
-      destruct (IHl (F acc a) x).
-      split ; intros.
-      apply H.
-      unfold F.
-      rewrite Pos.max_le_iff.
-      tauto.
-      destruct H1 ; subst.
-      apply H.
-      unfold F.
-      rewrite Pos.max_le_iff.
-      simpl.
-      left.
+
+Lemma max_var_le : forall p v,
+    (v <= max_var v p)%positive.
+Proof.
+  induction p; simpl.
+  - intros.
+    apply Pos.le_refl.
+  - intros.
+    specialize (IHp (p+v)%positive).
+    eapply Pos.le_trans ; eauto.
+    assert (xH + v <= p + v)%positive.
+    { apply Pos.add_le_mono.
+      apply Pos.le_1_l.
       apply Pos.le_refl.
-      tauto.
     }
-    tauto.
-  Qed.
+    eapply Pos.le_trans ; eauto.
+    apply pos_le_add.
+  - intros.
+    apply Pos.max_case_strong;intros ; auto.
+    specialize (IHp2 (Pos.succ v)%positive).
+    eapply Pos.le_trans ; eauto.
+Qed.
+
+Lemma max_var_correct : forall p j v,
+    In v (vars j p) -> Pos.le v (max_var j p).
+Proof.
+  induction p; simpl.
+  - tauto.
+  - auto.
+  - intros.
+    rewrite in_app_iff in H.
+    destruct H as [H |[ H | H]].
+    + subst.
+      apply Pos.max_case_strong;intros ; auto.
+      apply max_var_le.
+      eapply Pos.le_trans ; eauto.
+      apply max_var_le.
+    + apply Pos.max_case_strong;intros ; auto.
+      eapply Pos.le_trans ; eauto.
+    + apply Pos.max_case_strong;intros ; auto.
+      eapply Pos.le_trans ; eauto.
+Qed.
+
+Definition max_var_nformulae (l : list (NFormula Z)) :=
+  List.fold_left  (fun acc f => Pos.max acc (max_var xH (fst f))) l xH.
 
-  Definition is_subset (v1 v2 : t) :=
-    forall x, mem x v1 = true -> mem x v2 = true.
+Section MaxVar.
 
-  Lemma is_subset_union_l : forall v1 v2,
-      is_subset v1 (union v1 v2).
+  Definition F (acc : positive) (f : Pol Z * Op1) := Pos.max acc (max_var 1 (fst f)).
+
+  Lemma max_var_nformulae_mono_aux :
+    forall l v acc,
+      (v <= acc ->
+       v <= fold_left F l acc)%positive.
   Proof.
-    unfold is_subset.
+    induction l ; simpl ; [easy|].
     intros.
-    apply mem_union_l; auto.
+    apply IHl.
+    unfold F.
+    apply Pos.max_case_strong;intros ; auto.
+    eapply Pos.le_trans ; eauto.
   Qed.
 
-  Lemma is_subset_union_r : forall v1 v2,
-      is_subset v1 (union v2 v1).
+  Lemma max_var_nformulae_mono_aux' :
+    forall l acc acc',
+      (acc <= acc' ->
+       fold_left F l acc <= fold_left F l acc')%positive.
   Proof.
-    unfold is_subset.
+    induction l ; simpl ; [easy|].
     intros.
-    apply mem_union_r; auto.
+    apply IHl.
+    unfold F.
+    apply Pos.max_le_compat_r; auto.
   Qed.
 
 
-  End Vars.
-
-
-Fixpoint vars_of_pexpr (e : PExpr Z) : Vars.t :=
-  match e with
-  | PEc _ => Vars.empty
-  | PEX x => Vars.singleton x
-  | PEadd e1 e2 | PEsub e1 e2 | PEmul e1 e2 =>
-    let v1 := vars_of_pexpr e1 in
-    let v2 := vars_of_pexpr e2 in
-    Vars.union v1 v2
-  | PEopp c => vars_of_pexpr c
-  | PEpow e n => vars_of_pexpr e
-  end.
-
-Definition vars_of_formula (f : Formula Z) :=
-  match f with
-  | Build_Formula l o r =>
-    let v1 := vars_of_pexpr l in
-    let v2 := vars_of_pexpr r in
-    Vars.union v1 v2
-  end.
-
-Fixpoint vars_of_bformula {TX : Type} {TG : Type} {ID : Type}
-         (F : @GFormula (Formula Z) TX TG ID) : Vars.t :=
-  match F with
-  | TT  => Vars.empty
-  | FF  => Vars.empty
-  | X  p => Vars.empty
-  | A a t => vars_of_formula a
-  | Cj f1 f2 | D f1 f2 | I f1 _ f2 =>
-                         let v1 := vars_of_bformula f1 in
-                         let v2 := vars_of_bformula f2 in
-                         Vars.union v1 v2
-  | Tauto.N f     => vars_of_bformula f
-  end.
-
-Definition bound_var (v : positive) : Formula Z :=
-  Build_Formula (PEX v) OpGe (PEc 0).
-
-Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z :=
-  Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)).
-
-Section BOUND.
-  Context {TX TG ID : Type}.
 
-  Variable tag_of_var : positive -> positive -> option bool -> TG.
 
-  Definition bound_vars  (fr : positive)
-             (v : Vars.t) : @GFormula (Formula Z) TX TG ID :=
-    Vars.fold (fun k acc =>
-                 let y := (xO (fr + k)) in
-                 let z := (xI (fr + k)) in
-                 Cj
-                   (Cj (A (mk_eq_pos k y z) (tag_of_var fr k None))
-                       (Cj (A (bound_var y) (tag_of_var fr k (Some false)))
-                           (A (bound_var z) (tag_of_var fr k (Some true)))))
-                   acc) v TT.
+  Lemma max_var_nformulae_correct_aux : forall l p o v,
+      In (p,o) l -> In v (vars xH p) -> Pos.le v (fold_left F l 1)%positive.
+  Proof.
+  intros.
+  generalize 1%positive as acc.
+  revert p o v H H0.
+  induction l.
+  - simpl. tauto.
+  - simpl.
+    intros.
+    destruct H ; subst.
+    + unfold F at 2.
+      simpl.
+      apply max_var_correct in H0.
+      apply max_var_nformulae_mono_aux.
+      apply Pos.max_case_strong;intros ; auto.
+      eapply Pos.le_trans ; eauto.
+    + eapply IHl ; eauto.
+  Qed.
 
-  Definition bound_problem  (F : @GFormula (Formula Z) TX TG ID) : GFormula :=
-    let v := vars_of_bformula F in
-    I (bound_vars (Pos.succ (Vars.max_element v)) v) None F.
+End MaxVar.
 
+Lemma max_var_nformalae_correct : forall l p o v,
+      In (p,o) l -> In v (vars xH p) -> Pos.le v (max_var_nformulae l)%positive.
+Proof.
+  intros l p o v.
+  apply max_var_nformulae_correct_aux.
+Qed.
 
-  Definition bound_problem_fr (fr : positive) (F : @GFormula (Formula Z) TX TG ID) : GFormula :=
-    let v := vars_of_bformula F in
-    I (bound_vars fr v) None F.
 
+Fixpoint max_var_psatz (w : Psatz Z) : positive :=
+  match w with
+  | PsatzIn _ n => xH
+  | PsatzSquare p => max_var xH (Psquare 0 1 Z.add Z.mul Zeq_bool p)
+  | PsatzMulC p w => Pos.max (max_var xH p) (max_var_psatz w)
+  | PsatzMulE w1 w2 => Pos.max (max_var_psatz w1) (max_var_psatz w2)
+  | PsatzAdd w1 w2  => Pos.max (max_var_psatz w1) (max_var_psatz w2)
+  | _   => xH
+  end.
 
-End BOUND.
+Fixpoint max_var_prf (w : ZArithProof) : positive :=
+  match w with
+  | DoneProof => xH
+  | RatProof w pf | CutProof w pf => Pos.max (max_var_psatz w) (max_var_prf pf)
+  | EnumProof w1 w2 l => List.fold_left (fun acc prf => Pos.max acc (max_var_prf prf)) l
+                                        (Pos.max (max_var_psatz w1) (max_var_psatz w2))
+  | ExProof _ pf => max_var_prf pf
+  end.
 
 
 
-Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof)  {struct pf} : bool :=
+Fixpoint ZChecker  (l:list (NFormula Z)) (pf : ZArithProof)  {struct pf} : bool :=
   match pf with
     | DoneProof => false
     | RatProof w pf =>
@@ -1025,11 +1014,17 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof)  {struct pf} : bool :
             | Some cp => ZChecker (nformula_of_cutting_plane cp::l) pf
           end
       end
-(*    | SplitProof e pf1 pf2 =>
-      match ZChecker ((e,NonStrict)::l) pf1 , ZChecker ((
-*)
-
-    | EnumProof w1 w2 pf =>
+    | ExProof x prf =>
+      let fr := max_var_nformulae l in
+      if Pos.leb x fr then
+      let z    := Pos.succ fr in
+      let t    := Pos.succ z in
+      let nfx  := xnnormalise (mk_eq_pos x z t) in
+      let posz := xnnormalise (bound_var z) in
+      let post := xnnormalise (bound_var t) in
+      ZChecker (nfx::posz::post::l) prf
+      else false
+      | EnumProof w1 w2 pf =>
        match eval_Psatz l w1 , eval_Psatz l w2 with
          |  Some f1 , Some f2 =>
            match genCuttingPlane f1 , genCuttingPlane f2 with
@@ -1040,7 +1035,7 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof)  {struct pf} : bool :
                    fun lb ub =>
                      match pfs with
                        | nil => if Z.gtb lb ub then true else false
-                       | pf::rsr => andb (ZChecker  ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Z.add lb 1%Z) ub)
+                       | pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Z.add lb 1%Z) ub)
                      end)   pf (Z.opp z1)  z2
                   else false
               |   _    ,   _   => true
@@ -1057,6 +1052,7 @@ Fixpoint bdepth (pf : ZArithProof) : nat :=
     | RatProof _ p =>  S (bdepth p)
     | CutProof _  p =>   S  (bdepth p)
     | EnumProof _ _ l => S (List.fold_right (fun pf x => Nat.max (bdepth pf) x)   O l)
+    | ExProof _ p   => S (bdepth p)
   end.
 
 Require Import Wf_nat.
@@ -1246,16 +1242,190 @@ Proof.
   destruct (makeCuttingPlane p) ; discriminate.
 Qed.
 
+Lemma eval_nformula_mk_eq_pos : forall env x z t,
+    env x = env z - env t ->
+    eval_nformula env (xnnormalise (mk_eq_pos x z t)).
+Proof.
+  intros.
+  rewrite xnnormalise_correct.
+  simpl. auto.
+Qed.
+
+Lemma eval_nformula_bound_var : forall env x,
+    env x >= 0 ->
+    eval_nformula env (xnnormalise (bound_var x)).
+Proof.
+  intros.
+  rewrite xnnormalise_correct.
+  simpl. auto.
+Qed.
+
+
+Definition agree_env (fr : positive) (env env' : positive -> Z) : Prop :=
+  forall x, Pos.le x fr -> env x = env' x.
+
+Lemma agree_env_subset : forall v1 v2 env env',
+    agree_env v1 env env' ->
+    Pos.le v2 v1 ->
+    agree_env v2 env env'.
+Proof.
+  unfold agree_env.
+  intros.
+  apply H.
+  eapply Pos.le_trans ; eauto.
+Qed.
+
+
+Lemma agree_env_jump : forall fr j env env',
+    agree_env (fr + j) env env' ->
+    agree_env fr (Env.jump j env) (Env.jump j env').
+Proof.
+  intros.
+  unfold agree_env ; intro.
+  intros.
+  unfold Env.jump.
+  apply H.
+  apply Pos.add_le_mono_r; auto.
+Qed.
+
+
+Lemma agree_env_tail : forall fr env env',
+    agree_env (Pos.succ fr) env env' ->
+    agree_env fr (Env.tail env) (Env.tail env').
+Proof.
+  intros.
+  unfold Env.tail.
+  apply agree_env_jump.
+  rewrite <- Pos.add_1_r in H.
+  apply H.
+Qed.
+
+
+Lemma max_var_acc : forall p i j,
+    (max_var (i + j) p = max_var i p + j)%positive.
+Proof.
+  induction p; simpl.
+  - reflexivity.
+  - intros.
+    rewrite ! IHp.
+    rewrite Pos.add_assoc.
+    reflexivity.
+  - intros.
+    rewrite !Pplus_one_succ_l.
+    rewrite ! IHp1.
+    rewrite ! IHp2.
+    rewrite ! Pos.add_assoc.
+    rewrite <- Pos.add_max_distr_r.
+    reflexivity.
+Qed.
+
+
+
+Lemma agree_env_eval_nformula :
+  forall env env' e
+         (AGREE : agree_env (max_var xH (fst e))  env env'),
+    eval_nformula env e  <->  eval_nformula env' e.
+Proof.
+  destruct e.
+  simpl; intros.
+  assert ((RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env p)
+          =
+          (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)).
+  {
+    revert env env' AGREE.
+    generalize xH.
+    induction p ; simpl.
+    - reflexivity.
+    - intros.
+      apply IHp with (p := p1%positive).
+      apply agree_env_jump.
+      eapply agree_env_subset; eauto.
+      rewrite (Pos.add_comm p).
+      rewrite max_var_acc.
+      apply Pos.le_refl.
+    - intros.
+      f_equal.
+      f_equal.
+      { apply IHp1 with (p:= p).
+        eapply agree_env_subset; eauto.
+        apply Pos.le_max_l.
+      }
+      f_equal.
+      { unfold Env.hd.
+        unfold Env.nth.
+        apply AGREE.
+        apply Pos.le_1_l.
+      }
+      {
+        apply IHp2 with (p := p).
+        apply agree_env_tail.
+        eapply agree_env_subset; eauto.
+        rewrite !Pplus_one_succ_r.
+        rewrite max_var_acc.
+        apply Pos.le_max_r.
+      }
+  }
+  rewrite H. tauto.
+Qed.
+
+Lemma agree_env_eval_nformulae :
+  forall env env' l
+         (AGREE : agree_env (max_var_nformulae l) env env'),
+         make_conj (eval_nformula env) l <->
+         make_conj (eval_nformula env') l.
+Proof.
+  induction l.
+  - simpl. tauto.
+  - intros.
+    rewrite ! make_conj_cons.
+    assert (eval_nformula env a <-> eval_nformula env' a).
+    {
+      apply agree_env_eval_nformula.
+      eapply agree_env_subset ; eauto.
+      unfold max_var_nformulae.
+      simpl.
+      rewrite Pos.max_1_l.
+      apply max_var_nformulae_mono_aux.
+      apply Pos.le_refl.
+    }
+    rewrite H.
+    apply  and_iff_compat_l.
+    apply IHl.
+    eapply agree_env_subset ; eauto.
+    unfold max_var_nformulae.
+    simpl.
+    apply max_var_nformulae_mono_aux'.
+    apply Pos.le_1_l.
+Qed.
 
-Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl  (eval_nformula env)  l False.
+
+Lemma eq_true_iff_eq :
+  forall b1 b2 : bool, (b1 = true <-> b2 = true) <-> b1 = b2.
+Proof.
+  destruct b1,b2 ; intuition congruence.
+Qed.
+
+Ltac pos_tac :=
+  repeat
+  match goal with
+  | |- false = _ => symmetry
+  | |- Pos.eqb ?X ?Y = false => rewrite Pos.eqb_neq ; intro
+  | H : @eq positive ?X ?Y |- _ =>  apply Zpos_eq in H
+  | H : context[Z.pos (Pos.succ ?X)] |- _ => rewrite (Pos2Z.inj_succ X) in H
+  | H : Pos.leb ?X ?Y = true |- _ => rewrite Pos.leb_le in H ;
+                                     apply (Pos2Z.pos_le_pos X Y) in H
+  end.
+
+Lemma ZChecker_sound : forall w l,
+    ZChecker l w = true -> forall env, make_impl  (eval_nformula env)  l False.
 Proof.
   induction w    using (well_founded_ind (well_founded_ltof _ bdepth)).
-  destruct w as [ | w pf | w pf | w1 w2 pf].
-  (* DoneProof *)
+  destruct w as [ | w pf | w pf | w1 w2 pf | x pf].
+  - (* DoneProof *)
   simpl. discriminate.
-  (* RatProof *)
+  - (* RatProof *)
   simpl.
-  intro l. case_eq (eval_Psatz l w) ; [| discriminate].
+  intros l. case_eq (eval_Psatz l w) ; [| discriminate].
   intros f Hf.
   case_eq (Zunsat f).
   intros.
@@ -1276,15 +1446,15 @@ Proof.
   apply H2.
   split ; auto.
   apply eval_Psatz_sound with (2:= Hf) ; assumption.
-  (* CutProof *)
+  - (* CutProof *)
   simpl.
-  intro l.
+  intros l.
   case_eq (eval_Psatz l w) ; [ | discriminate].
   intros f' Hlc.
   case_eq (genCuttingPlane f').
   intros.
   assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False).
-   eapply (H pf) ; auto.
+   eapply (H pf)  ; auto.
    unfold ltof.
    simpl.
    auto with arith.
@@ -1303,8 +1473,8 @@ Proof.
   intros.
   apply eval_Psatz_sound with (2:= Hlc) in H2.
   apply genCuttingPlaneNone with (2:= H2) ; auto.
-  (* EnumProof *)
-  intro.
+  - (* EnumProof *)
+  intros l.
   simpl.
   case_eq (eval_Psatz l w1) ; [  | discriminate].
   case_eq (eval_Psatz l w2) ; [  | discriminate].
@@ -1359,7 +1529,7 @@ Proof.
   intros.
   assert (HH :forall x, -z1 <= x <= z2 -> exists pr,
     (In pr pf /\
-      ZChecker  ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z).
+      ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z).
   clear HZ0 Hop1 Hop2 HCutL HCutR H0 H1.
   revert Hfix.
   generalize (-z1). clear z1. intro z1.
@@ -1386,7 +1556,7 @@ Proof.
   (*/asser *)
   destruct (HH _ H1) as [pr [Hin Hcheker]].
   assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False).
-   apply (H pr);auto.
+   eapply (H pr)  ;auto.
    apply in_bdepth ; auto.
   rewrite <- make_conj_impl in H2.
   apply H2.
@@ -1410,6 +1580,92 @@ Proof.
   intros.
   apply eval_Psatz_sound with (2:= Hf2) in H2.
   apply genCuttingPlaneNone with (2:= H2) ; auto.
+- intros l.
+  unfold ZChecker.
+  fold ZChecker.
+  set (fr := (max_var_nformulae l)%positive).
+  set (z1 := (Pos.succ fr)) in *.
+  set (t1 := (Pos.succ z1)) in *.
+  destruct (x <=? fr)%positive eqn:LE ; [|congruence].
+  intros.
+  set (env':= fun v => if Pos.eqb v z1
+                       then if Z.leb (env x) 0 then 0 else env x
+                       else if Pos.eqb v t1
+                            then if Z.leb (env x) 0 then -(env x) else 0
+                            else env v).
+  apply H with (env:=env') in H0.
+  + rewrite <- make_conj_impl in *.
+    intro.
+    rewrite !make_conj_cons in H0.
+    apply H0 ; repeat split.
+    *
+      apply eval_nformula_mk_eq_pos.
+      unfold env'.
+      rewrite! Pos.eqb_refl.
+      replace (x=?z1)%positive with false.
+      replace (x=?t1)%positive with false.
+      replace (t1=?z1)%positive with false.
+      destruct (env x <=? 0); ring.
+      { unfold t1.
+        pos_tac; normZ.
+        lia (Hyp H2).
+      }
+      {
+        unfold t1, z1.
+        pos_tac; normZ.
+        lia (Add (Hyp LE) (Hyp H3)).
+      }
+      {
+        unfold z1.
+        pos_tac; normZ.
+        lia (Add (Hyp LE) (Hyp H3)).
+      }
+    *
+      apply eval_nformula_bound_var.
+      unfold env'.
+      rewrite! Pos.eqb_refl.
+      destruct (env x <=? 0) eqn:EQ.
+      compute. congruence.
+      rewrite Z.leb_gt in EQ.
+      normZ.
+      lia (Add (Hyp EQ) (Hyp H2)).
+    *
+      apply eval_nformula_bound_var.
+      unfold env'.
+      rewrite! Pos.eqb_refl.
+      replace (t1 =? z1)%positive with false.
+      destruct (env x <=? 0) eqn:EQ.
+      rewrite Z.leb_le in EQ.
+      normZ.
+      lia (Add (Hyp EQ) (Hyp H2)).
+      compute; congruence.
+      unfold t1.
+      clear.
+      pos_tac; normZ.
+      lia (Hyp H).
+    *
+      rewrite agree_env_eval_nformulae with (env':= env') in H1;auto.
+      unfold agree_env; intros.
+      unfold env'.
+      replace (x0 =? z1)%positive with false.
+      replace (x0 =? t1)%positive with false.
+      reflexivity.
+      {
+        unfold t1, z1.
+        unfold fr in *.
+        apply Pos2Z.pos_le_pos in H2.
+        pos_tac; normZ.
+        lia (Add (Hyp H2) (Hyp H4)).
+      }
+      {
+        unfold z1, fr in *.
+        apply Pos2Z.pos_le_pos in H2.
+        pos_tac; normZ.
+        lia (Add (Hyp H2) (Hyp H4)).
+      }
+  + unfold ltof.
+    simpl.
+    apply Nat.lt_succ_diag_r.
 Qed.
 
 
@@ -1417,7 +1673,7 @@ Qed.
 Definition ZTautoChecker  (f : BFormula (Formula Z)) (w: list ZArithProof): bool :=
   @tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate  ZArithProof (fun cl => ZChecker (List.map fst cl)) f w.
 
-Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_f (fun x => x) (Zeval_formula env)  f.
+Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_bf  (Zeval_formula env)  f.
 Proof.
   intros f w.
   unfold ZTautoChecker.
@@ -1430,11 +1686,12 @@ Proof.
   - unfold Zdeduce. intros. revert H.
      apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto.
   -
-    intros env t tg.
-    rewrite normalise_correct ; auto.
+    intros.
+    rewrite normalise_correct  in H.
+    auto.
   -
-    intros env t tg.
-    rewrite negate_correct ; auto.
+    intros.
+    rewrite negate_correct in H ; auto.
   - intros t w0.
     unfold eval_tt.
     intros.
@@ -1443,270 +1700,6 @@ Proof.
     tauto.
 Qed.
 
-Record is_diff_env_elt (fr : positive) (env env' : positive -> Z) (x:positive):=
-  {
-    eq_env  : env x = env' x;
-    eq_diff : env x = env' (xO (fr+ x)) - env' (xI (fr + x));
-    pos_xO  : env' (xO (fr+x)) >= 0;
-    pos_xI  : env' (xI (fr+x)) >= 0;
-  }.
-
-
-Definition is_diff_env  (s : Vars.t) (env env' : positive -> Z) :=
-  let fr := Pos.succ (Vars.max_element s) in
-  forall x, Vars.mem x s = true ->
-            is_diff_env_elt fr env env' x.
-
-Definition mk_diff_env  (s : Vars.t) (env : positive -> Z) :=
-  let fr := Vars.max_element s in
-  fun x =>
-    if Pos.leb x fr
-    then env x
-    else
-      let fr' := Pos.succ fr in
-      match x with
-      | xO x => if Z.leb (env (x - fr')%positive) 0
-                then 0 else env (x -fr')%positive
-      | xI x => if Z.leb (env (x - fr')%positive) 0
-                then - (env (x - fr')%positive) else 0
-      | xH   => 0
-      end.
-
-Lemma le_xO : forall x, (x <= xO x)%positive.
-Proof.
-  intros.
-  change x with (1 * x)%positive at 1.
-  change (xO x) with (2 * x)%positive.
-  apply Pos.mul_le_mono.
-  compute. congruence.
-  apply Pos.le_refl.
-Qed.
-
-Lemma leb_xO_false :
-  (forall x y,  x <=? y = false ->
-             xO x <=? y = false)%positive.
-Proof.
-  intros.
-  rewrite Pos.leb_nle in *.
-  intro. apply H.
-  eapply Pos.le_trans ; eauto.
-  apply le_xO.
-Qed.
-
-Lemma leb_xI_false :
-  (forall x y,  x <=? y = false ->
-             xI x <=? y = false)%positive.
-Proof.
-  intros.
-  rewrite Pos.leb_nle in *.
-  intro. apply H.
-  eapply Pos.le_trans ; eauto.
-  generalize (le_xO x).
-  intros.
-  eapply Pos.le_trans ; eauto.
-  change (xI x) with (Pos.succ (xO x))%positive.
-  apply Pos.lt_le_incl.
-  apply Pos.lt_succ_diag_r.
-Qed.
-
-Lemma is_diff_env_ex : forall s env,
-    is_diff_env s env (mk_diff_env s env).
-Proof.
-  intros.
-  unfold is_diff_env, mk_diff_env.
-  intros.
-  assert
-    ((Pos.succ (Vars.max_element s) + x <=? Vars.max_element s  = false)%positive).
-  {
-      rewrite Pos.leb_nle.
-      intro.
-      eapply (Pos.lt_irrefl (Pos.succ (Vars.max_element s) + x)).
-      eapply Pos.le_lt_trans ; eauto.
-      generalize (Pos.lt_succ_diag_r (Vars.max_element s)).
-      intro.
-      eapply Pos.lt_trans ; eauto.
-      apply Pos.lt_add_r.
-  }
-  constructor.
-  - apply Vars.max_element_max in H.
-    rewrite <- Pos.leb_le   in H.
-    rewrite H. auto.
-  -
-    rewrite  leb_xO_false by auto.
-    rewrite leb_xI_false by auto.
-    rewrite Pos.add_comm.
-    rewrite Pos.add_sub.
-    destruct (env x <=? 0); ring.
-  - rewrite  leb_xO_false by auto.
-    rewrite Pos.add_comm.
-    rewrite Pos.add_sub.
-    destruct (env x <=? 0) eqn:EQ.
-    apply Z.le_ge.
-    apply Z.le_refl.
-    rewrite Z.leb_gt in EQ.
-    apply Z.le_ge.
-    apply Z.lt_le_incl.
-    auto.
-  - rewrite  leb_xI_false by auto.
-    rewrite Pos.add_comm.
-    rewrite Pos.add_sub.
-    destruct (env x <=? 0) eqn:EQ.
-    rewrite Z.leb_le in EQ.
-    apply Z.le_ge.
-    apply Z.opp_nonneg_nonpos; auto.
-    apply Z.le_ge.
-    apply Z.le_refl.
-Qed.
-
-Lemma env_bounds : forall tg env s,
-    let fr := Pos.succ (Vars.max_element s) in
-    exists env', is_diff_env s env env'
-                   /\
-                   eval_bf  (Zeval_formula env') (bound_vars tg fr s).
-Proof.
-  intros.
-  assert (DIFF:=is_diff_env_ex s env).
-  exists (mk_diff_env s env). split ; auto.
-  unfold bound_vars.
-  rewrite FSetPositive.PositiveSet.fold_1.
-  revert DIFF.
-  set (env' := mk_diff_env s env).
-  intro.
-  assert (ACC : eval_bf  (Zeval_formula env') TT ).
-  {
-    simpl. auto.
-  }
-  revert ACC.
-  match goal with
-  | |- context[@TT ?A ?B ?C ?D] => generalize (@TT A B C D) as acc
-  end.
-  unfold is_diff_env in DIFF.
-  assert (DIFFL : forall x, In x (FSetPositive.PositiveSet.elements s) ->
-                            (x < fr)%positive /\
-                            is_diff_env_elt fr env env' x).
-  {
-    intros.
-    rewrite <- Vars.mem_elements in H.
-    split.
-    apply Vars.max_element_max in H.
-    unfold fr in *.
-    eapply Pos.le_lt_trans ; eauto.
-    apply Pos.lt_succ_diag_r.
-    apply DIFF; auto.
-  }
-  clear DIFF.
-  match goal with
-  | |- context[fold_left ?F _ _] =>
-    set (FUN := F)
-  end.
-  induction (FSetPositive.PositiveSet.elements s).
-  - simpl; auto.
-  - simpl.
-    intros.
-    eapply IHl ; eauto.
-    + intros. apply DIFFL.
-      simpl ; auto.
-    + unfold FUN.
-      simpl.
-      split ; auto.
-      assert (HYP : (a < fr /\ is_diff_env_elt fr env env' a)%positive).
-      {
-        apply DIFFL.
-        simpl.  tauto.
-      }
-      destruct HYP as (LT & DIFF).
-      destruct DIFF.
-      rewrite <- eq_env0.
-      tauto.
-Qed.
-
-Definition agree_env (v : Vars.t) (env env' : positive -> Z) : Prop :=
-  forall x, Vars.mem x v = true -> env x = env' x.
-
-Lemma agree_env_subset : forall s1 s2 env env',
-    agree_env s1 env env' ->
-    Vars.is_subset s2 s1 ->
-    agree_env s2 env env'.
-Proof.
-  unfold agree_env.
-  intros.
-  apply H. apply H0; auto.
-Qed.
-
-Lemma agree_env_union : forall s1 s2 env env',
-    agree_env (Vars.union s1 s2) env env' ->
-    agree_env s1 env env' /\ agree_env s2 env env'.
-Proof.
-  split;
-  eapply agree_env_subset; eauto.
-  apply Vars.is_subset_union_l.
-  apply Vars.is_subset_union_r.
-Qed.
-
-
-
-Lemma agree_env_eval_expr :
-  forall env env' e
-         (AGREE : agree_env (vars_of_pexpr e)  env env'),
-  Zeval_expr env e =  Zeval_expr env' e.
-Proof.
-  induction e; simpl;intros;
-    try (apply agree_env_union in AGREE; destruct AGREE);  try f_equal ; auto.
-  - intros ; apply AGREE.
-    apply Vars.mem_singleton.
-Qed.
-
-Lemma agree_env_eval_bf :
-  forall env env' f
-         (AGREE: agree_env (vars_of_bformula f) env env'),
-    eval_bf (Zeval_formula env') f <->
-    eval_bf (Zeval_formula env) f.
-Proof.
-  induction f; simpl; intros ;
-    try (apply agree_env_union in AGREE; destruct AGREE) ; try intuition fail.
-  -
-    unfold Zeval_formula.
-    destruct t.
-    simpl in * ; intros.
-    apply agree_env_union in AGREE ; destruct AGREE.
-    rewrite <- agree_env_eval_expr with (env:=env) by auto.
-    rewrite <- agree_env_eval_expr with (e:= Frhs) (env:=env) by auto.
-    tauto.
-Qed.
-
-Lemma bound_problem_sound : forall tg f,
-    (forall env' : PolEnv Z,
-        eval_bf  (Zeval_formula env')
-                 (bound_problem tg f)) ->
-    forall env,
-      eval_bf (Zeval_formula env) f.
-Proof.
-  intros.
-  unfold bound_problem in H.
-  destruct (env_bounds tg env (vars_of_bformula f))
-           as (env' & DIFF & EVAL).
-  simpl in H.
-  apply H in EVAL.
-  eapply agree_env_eval_bf ; eauto.
-  unfold is_diff_env, agree_env in *.
-  intros.
-  apply DIFF in H0.
-  destruct H0.
-  intuition.
-Qed.
-
-
-
-Definition ZTautoCheckerExt (f : BFormula (Formula Z)) (w : list ZArithProof) : bool :=
-  ZTautoChecker (bound_problem (fun _ _ _ => tt) f) w.
-
-Lemma ZTautoCheckerExt_sound : forall f w, ZTautoCheckerExt f w = true -> forall env, eval_bf (Zeval_formula env)  f.
-Proof.
-  intros.
-  unfold ZTautoCheckerExt in H.
-  specialize (ZTautoChecker_sound _ _ H).
-  intros ; apply bound_problem_sound with (tg:= fun _ _ _ => tt); auto.
-Qed.
 
 Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof)  : list nat :=
   match pt with
@@ -1716,6 +1709,7 @@ Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof)  : list nat :=
     | EnumProof c1 c2 l =>
       let acc := xhyps_of_psatz base (xhyps_of_psatz base acc c2) c1 in
         List.fold_left (xhyps_of_pt (S base)) l acc
+    | ExProof _ pt  =>  xhyps_of_pt (S (S (S base ))) acc pt
   end.
 
 Definition hyps_of_pt (pt : ZArithProof) : list nat := xhyps_of_pt 0 nil pt.
diff --git a/plugins/micromega/Ztac.v b/plugins/micromega/Ztac.v
new file mode 100644
index 0000000000..091f58a0ef
--- /dev/null
+++ b/plugins/micromega/Ztac.v
@@ -0,0 +1,140 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Tactics for doing arithmetic proofs.
+    Useful to bootstrap lia.
+ *)
+
+Require Import ZArithRing.
+Require Import ZArith_base.
+Local Open Scope Z_scope.
+
+Lemma eq_incl :
+  forall (x y:Z), x = y -> x <= y /\ y <= x.
+Proof.
+  intros; split;
+  apply Z.eq_le_incl; auto.
+Qed.
+
+Lemma elim_concl_eq :
+  forall x y, (x < y \/ y < x -> False) -> x = y.
+Proof.
+  intros.
+  destruct (Z_lt_le_dec x y).
+  exfalso. apply H ; auto.
+  destruct (Zle_lt_or_eq y x);auto.
+  exfalso.
+  apply H ; auto.
+Qed.
+
+Lemma elim_concl_le :
+  forall x y, (y < x -> False) -> x <= y.
+Proof.
+  intros.
+  destruct (Z_lt_le_dec y x).
+  exfalso ; auto.
+  auto.
+Qed.
+
+Lemma elim_concl_lt :
+  forall x y, (y <= x -> False) -> x < y.
+Proof.
+  intros.
+  destruct (Z_lt_le_dec x y).
+  auto.
+  exfalso ; auto.
+Qed.
+
+
+
+Lemma Zlt_le_add_1 : forall n m : Z, n < m -> n + 1 <= m.
+Proof. exact (Zlt_le_succ). Qed.
+
+
+Ltac normZ :=
+  repeat
+  match goal with
+  | H : _ < _ |- _ =>  apply Zlt_le_add_1 in H
+  | H : ?Y <= _ |- _ =>
+    lazymatch Y with
+    | 0 => fail
+    | _ => apply Zle_minus_le_0 in H
+    end
+  | H : _ >= _ |- _ => apply Z.ge_le in H
+  | H : _ > _  |- _ => apply Z.gt_lt in H
+  | H : _ = _  |- _ => apply eq_incl in H ; destruct H
+  | |- @eq Z _ _  => apply elim_concl_eq ; let H := fresh "HZ" in intros [H|H]
+  | |- _ <= _ => apply elim_concl_le ; intros
+  | |- _ < _ => apply elim_concl_lt ; intros
+  | |- _ >= _ => apply Z.le_ge
+  end.
+
+
+Inductive proof :=
+| Hyp (e : Z) (prf : 0 <= e)
+| Add (p1 p2: proof)
+| Mul (p1 p2: proof)
+| Cst (c : Z)
+.
+
+Lemma add_le : forall e1 e2, 0 <= e1 -> 0 <= e2 -> 0 <= e1+e2.
+Proof.
+  intros.
+  change 0 with (0+ 0).
+  apply Z.add_le_mono; auto.
+Qed.
+
+Lemma mul_le : forall e1 e2, 0 <= e1 -> 0 <= e2 -> 0 <= e1*e2.
+Proof.
+  intros.
+  change 0 with (0* e2).
+  apply Zmult_le_compat_r; auto.
+Qed.
+
+Fixpoint eval_proof (p : proof) : { e : Z | 0 <= e} :=
+  match p with
+  | Hyp e prf => exist _ e prf
+  | Add p1 p2 => let (e1,p1) := eval_proof p1 in
+                 let (e2,p2) := eval_proof p2 in
+                 exist _ _ (add_le _ _ p1 p2)
+  | Mul p1 p2  => let (e1,p1) := eval_proof p1 in
+                 let (e2,p2) := eval_proof p2 in
+                 exist _ _ (mul_le _ _ p1 p2)
+  | Cst c      =>  match Z_le_dec 0 c with
+                   | left prf => exist _ _ prf
+                   |  _       => exist _ _ Z.le_0_1
+                 end
+  end.
+
+Ltac lia_step p :=
+  let H := fresh in
+  let prf := (eval cbn - [Z.le Z.mul Z.opp Z.sub Z.add] in (eval_proof p)) in
+  match prf with
+  | @exist _ _ _ ?P =>  pose proof P as H
+  end ; ring_simplify in H.
+
+Ltac lia_contr :=
+  match goal with
+  | H : 0 <= - (Zpos _) |- _ =>
+    rewrite <- Z.leb_le in H;
+    compute in H ; discriminate
+  | H : 0 <= (Zneg _) |- _ =>
+    rewrite <- Z.leb_le in H;
+    compute in H ; discriminate
+  end.
+
+
+Ltac lia p :=
+  lia_step p ; lia_contr.
+
+Ltac slia H1 H2 :=
+  normZ ; lia (Add (Hyp _ H1) (Hyp _ H2)).
+
+Arguments Hyp {_} prf.
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index f14db40d45..92a2222cfa 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -285,6 +285,7 @@ module M = struct
   let coq_ratProof = lazy (constant "RatProof")
   let coq_cutProof = lazy (constant "CutProof")
   let coq_enumProof = lazy (constant "EnumProof")
+  let coq_ExProof = lazy (constant "ExProof")
   let coq_Zgt = lazy (z_constant "Z.gt")
   let coq_Zge = lazy (z_constant "Z.ge")
   let coq_Zle = lazy (z_constant "Z.le")
@@ -1420,6 +1421,9 @@ let rec dump_proof_term = function
       , [| dump_psatz coq_Z dump_z c1
          ; dump_psatz coq_Z dump_z c2
          ; dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |] )
+  | Micromega.ExProof (p, prf) ->
+    EConstr.mkApp
+      (Lazy.force coq_ExProof, [|dump_positive p; dump_proof_term prf|])
 
 let rec size_of_psatz = function
   | Micromega.PsatzIn _ -> 1
@@ -1437,6 +1441,7 @@ let rec size_of_pf = function
   | Micromega.EnumProof (p1, p2, l) ->
     size_of_psatz p1 + size_of_psatz p2
     + List.fold_left (fun acc p -> size_of_pf p + acc) 0 l
+  | Micromega.ExProof (_, a) -> size_of_pf a + 1
 
 let dump_proof_term t =
   if debug then Printf.printf "dump_proof_term %i\n" (size_of_pf t);
@@ -1455,6 +1460,8 @@ let rec pp_proof_term o = function
     Printf.fprintf o "EP[%a,%a,%a]" (pp_psatz pp_z) c1 (pp_psatz pp_z) c2
       (pp_list "[" "]" pp_proof_term)
       rst
+  | Micromega.ExProof (p, prf) ->
+    Printf.fprintf o "Ex[%a,%a]" pp_positive p pp_proof_term prf
 
 let rec parse_hyps gl parse_arith env tg hyps =
   match hyps with
@@ -1504,33 +1511,6 @@ let qq_domain_spec =
 let max_tag f =
   1 + Tag.to_int (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) f (Tag.from 0))
 
-(** For completeness of the cutting-plane procedure,
-    each variable 'x' is replaced by 'y' - 'z' where
-    'y' and 'z' are positive *)
-let pre_processZ mt f =
-  let x0 i = 2 * i in
-  let x1 i = (2 * i) + 1 in
-  let tag_of_var fr p b =
-    let ip = CoqToCaml.positive fr + CoqToCaml.positive p in
-    match b with
-    | None ->
-      let y = Mc.XO (Mc.Coq_Pos.add fr p) in
-      let z = Mc.XI (Mc.Coq_Pos.add fr p) in
-      let tag = Tag.from (-x0 (x0 ip)) in
-      let constr = Mc.mk_eq_pos p y z in
-      (tag, dump_cstr (Lazy.force coq_Z) dump_z constr)
-    | Some false ->
-      let y = Mc.XO (Mc.Coq_Pos.add fr p) in
-      let tag = Tag.from (-x0 (x1 ip)) in
-      let constr = Mc.bound_var (Mc.XO y) in
-      (tag, dump_cstr (Lazy.force coq_Z) dump_z constr)
-    | Some true ->
-      let z = Mc.XI (Mc.Coq_Pos.add fr p) in
-      let tag = Tag.from (-x1 (x1 ip)) in
-      let constr = Mc.bound_var (Mc.XI z) in
-      (tag, dump_cstr (Lazy.force coq_Z) dump_z constr)
-  in
-  Mc.bound_problem_fr tag_of_var mt f
 (** Naive topological sort of constr according to the subterm-ordering *)
 
 (* An element is minimal x is minimal w.r.t y if
@@ -2225,6 +2205,7 @@ let hyps_of_pt pt =
     | Mc.EnumProof (c1, c2, l) ->
       let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in
       List.fold_left (fun s x -> xhyps (base + 1) x s) s l
+    | Mc.ExProof (_, pt) -> xhyps (base + 3) pt acc
   in
   xhyps 0 pt ISet.empty
 
@@ -2242,6 +2223,7 @@ let compact_pt pt f =
         ( compact_cone c1 (translate ofset)
         , compact_cone c2 (translate ofset)
         , Mc.map (fun x -> compact_pt (ofset + 1) x) l )
+    | Mc.ExProof (x, pt) -> Mc.ExProof (x, compact_pt (ofset + 3) pt)
   in
   compact_pt 0 pt
 
@@ -2418,8 +2400,9 @@ let sos_Q =
 let sos_R = micromega_genr (non_linear_prover_R "pure_sos" None)
 
 let xlia =
-  micromega_gen parse_zarith pre_processZ Mc.cnfZ zz_domain_spec dump_zexpr
-    linear_Z
+  micromega_gen parse_zarith
+    (fun _ x -> x)
+    Mc.cnfZ zz_domain_spec dump_zexpr linear_Z
 
 let xnlia =
   micromega_gen parse_zarith
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index f508b3dc56..d17a0aabb7 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -281,6 +281,20 @@ module Coq_Pos =
   let compare =
     compare_cont Eq
 
+  (** val max : positive -> positive -> positive **)
+
+  let max p p' =
+    match compare p p' with
+    | Gt -> p
+    | _ -> p'
+
+  (** val leb : positive -> positive -> bool **)
+
+  let leb x y =
+    match compare x y with
+    | Gt -> false
+    | _ -> true
+
   (** val gcdn : nat -> positive -> positive -> positive **)
 
   let rec gcdn n0 a b =
@@ -1760,13 +1774,6 @@ let simpl_cone cO cI ctimes ceqb e = match e with
            | _ -> PsatzAdd (t1, t2)))
 | _ -> e
 
-module PositiveSet =
- struct
-  type tree =
-  | Leaf
-  | Node of tree * bool * tree
- end
-
 type q = { qnum : z; qden : positive }
 
 (** val qeq_bool : q -> q -> bool **)
@@ -1980,6 +1987,7 @@ type zArithProof =
 | RatProof of zWitness * zArithProof
 | CutProof of zWitness * zArithProof
 | EnumProof of zWitness * zWitness * zArithProof list
+| ExProof of positive * zArithProof
 
 (** val zgcdM : z -> z -> z **)
 
@@ -2051,116 +2059,6 @@ let valid_cut_sign = function
 | NonStrict -> true
 | _ -> false
 
-module Vars =
- struct
-  type elt = positive
-
-  type tree = PositiveSet.tree =
-  | Leaf
-  | Node of tree * bool * tree
-
-  type t = tree
-
-  (** val empty : t **)
-
-  let empty =
-    Leaf
-
-  (** val add : elt -> t -> t **)
-
-  let rec add i = function
-  | Leaf ->
-    (match i with
-     | XI i0 -> Node (Leaf, false, (add i0 Leaf))
-     | XO i0 -> Node ((add i0 Leaf), false, Leaf)
-     | XH -> Node (Leaf, true, Leaf))
-  | Node (l, o, r) ->
-    (match i with
-     | XI i0 -> Node (l, o, (add i0 r))
-     | XO i0 -> Node ((add i0 l), o, r)
-     | XH -> Node (l, true, r))
-
-  (** val singleton : elt -> t **)
-
-  let singleton i =
-    add i empty
-
-  (** val union : t -> t -> t **)
-
-  let rec union m m' =
-    match m with
-    | Leaf -> m'
-    | Node (l, o, r) ->
-      (match m' with
-       | Leaf -> m
-       | Node (l', o', r') ->
-         Node ((union l l'), (if o then true else o'), (union r r')))
-
-  (** val rev_append : elt -> elt -> elt **)
-
-  let rec rev_append y x =
-    match y with
-    | XI y0 -> rev_append y0 (XI x)
-    | XO y0 -> rev_append y0 (XO x)
-    | XH -> x
-
-  (** val rev : elt -> elt **)
-
-  let rev x =
-    rev_append x XH
-
-  (** val xfold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> elt -> 'a1 **)
-
-  let rec xfold f m v i =
-    match m with
-    | Leaf -> v
-    | Node (l, b, r) ->
-      if b
-      then xfold f r (f (rev i) (xfold f l v (XO i))) (XI i)
-      else xfold f r (xfold f l v (XO i)) (XI i)
-
-  (** val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 **)
-
-  let fold f m i =
-    xfold f m i XH
- end
-
-(** val vars_of_pexpr : z pExpr -> Vars.t **)
-
-let rec vars_of_pexpr = function
-| PEc _ -> Vars.empty
-| PEX x -> Vars.singleton x
-| PEadd (e1, e2) ->
-  let v1 = vars_of_pexpr e1 in let v2 = vars_of_pexpr e2 in Vars.union v1 v2
-| PEsub (e1, e2) ->
-  let v1 = vars_of_pexpr e1 in let v2 = vars_of_pexpr e2 in Vars.union v1 v2
-| PEmul (e1, e2) ->
-  let v1 = vars_of_pexpr e1 in let v2 = vars_of_pexpr e2 in Vars.union v1 v2
-| PEopp c -> vars_of_pexpr c
-| PEpow (e0, _) -> vars_of_pexpr e0
-
-(** val vars_of_formula : z formula -> Vars.t **)
-
-let vars_of_formula f =
-  let { flhs = l; fop = _; frhs = r } = f in
-  let v1 = vars_of_pexpr l in let v2 = vars_of_pexpr r in Vars.union v1 v2
-
-(** val vars_of_bformula : (z formula, 'a1, 'a2, 'a3) gFormula -> Vars.t **)
-
-let rec vars_of_bformula = function
-| A (a, _) -> vars_of_formula a
-| Cj (f1, f2) ->
-  let v1 = vars_of_bformula f1 in
-  let v2 = vars_of_bformula f2 in Vars.union v1 v2
-| D (f1, f2) ->
-  let v1 = vars_of_bformula f1 in
-  let v2 = vars_of_bformula f2 in Vars.union v1 v2
-| N f0 -> vars_of_bformula f0
-| I (f1, _, f2) ->
-  let v1 = vars_of_bformula f1 in
-  let v2 = vars_of_bformula f2 in Vars.union v1 v2
-| _ -> Vars.empty
-
 (** val bound_var : positive -> z formula **)
 
 let bound_var v =
@@ -2171,24 +2069,18 @@ let bound_var v =
 let mk_eq_pos x y t0 =
   { flhs = (PEX x); fop = OpEq; frhs = (PEsub ((PEX y), (PEX t0))) }
 
-(** val bound_vars :
-    (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z
-    formula, 'a1, 'a2, 'a3) gFormula **)
+(** val max_var : positive -> z pol -> positive **)
 
-let bound_vars tag_of_var fr v =
-  Vars.fold (fun k acc ->
-    let y = XO (Coq_Pos.add fr k) in
-    let z0 = XI (Coq_Pos.add fr k) in
-    Cj ((Cj ((A ((mk_eq_pos k y z0), (tag_of_var fr k None))), (Cj ((A
-    ((bound_var y), (tag_of_var fr k (Some false)))), (A ((bound_var z0),
-    (tag_of_var fr k (Some true)))))))), acc)) v TT
+let rec max_var jmp = function
+| Pc _ -> jmp
+| Pinj (j, p2) -> max_var (Coq_Pos.add j jmp) p2
+| PX (p2, _, q0) ->
+  Coq_Pos.max (max_var jmp p2) (max_var (Coq_Pos.succ jmp) q0)
 
-(** val bound_problem_fr :
-    (positive -> positive -> bool option -> 'a2) -> positive -> (z formula,
-    'a1, 'a2, 'a3) gFormula -> (z formula, 'a1, 'a2, 'a3) gFormula **)
+(** val max_var_nformulae : z nFormula list -> positive **)
 
-let bound_problem_fr tag_of_var fr f =
-  let v = vars_of_bformula f in I ((bound_vars tag_of_var fr v), None, f)
+let max_var_nformulae l =
+  fold_left (fun acc f -> Coq_Pos.max acc (max_var XH (fst f))) l XH
 
 (** val zChecker : z nFormula list -> zArithProof -> bool **)
 
@@ -2232,6 +2124,16 @@ let rec zChecker l = function
          | None -> true)
       | None -> false)
    | None -> false)
+| ExProof (x, prf) ->
+  let fr = max_var_nformulae l in
+  if Coq_Pos.leb x fr
+  then let z0 = Coq_Pos.succ fr in
+       let t0 = Coq_Pos.succ z0 in
+       let nfx = xnnormalise (mk_eq_pos x z0 t0) in
+       let posz = xnnormalise (bound_var z0) in
+       let post = xnnormalise (bound_var t0) in
+       zChecker (nfx::(posz::(post::l))) prf
+  else false
 
 (** val zTautoChecker : z formula bFormula -> zArithProof list -> bool **)
 
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 033f5d8732..4200c80574 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -47,6 +47,8 @@ module Coq_Pos : sig
   val size_nat : positive -> nat
   val compare_cont : comparison -> positive -> positive -> comparison
   val compare : positive -> positive -> comparison
+  val max : positive -> positive -> positive
+  val leb : positive -> positive -> bool
   val gcdn : nat -> positive -> positive -> positive
   val gcd : positive -> positive -> positive
   val of_succ_nat : nat -> positive
@@ -624,10 +626,6 @@ val simpl_cone :
   -> 'a1 psatz
   -> 'a1 psatz
 
-module PositiveSet : sig
-  type tree = Leaf | Node of tree * bool * tree
-end
-
 type q = {qnum : z; qden : positive}
 
 val qeq_bool : q -> q -> bool
@@ -672,6 +670,7 @@ type zArithProof =
   | RatProof of zWitness * zArithProof
   | CutProof of zWitness * zArithProof
   | EnumProof of zWitness * zWitness * zArithProof list
+  | ExProof of positive * zArithProof
 
 val zgcdM : z -> z -> z
 val zgcd_pol : z polC -> z * z
@@ -682,40 +681,10 @@ val nformula_of_cutting_plane : (z polC * z) * op1 -> z nFormula
 val is_pol_Z0 : z polC -> bool
 val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option
 val valid_cut_sign : op1 -> bool
-
-module Vars : sig
-  type elt = positive
-  type tree = PositiveSet.tree = Leaf | Node of tree * bool * tree
-  type t = tree
-
-  val empty : t
-  val add : elt -> t -> t
-  val singleton : elt -> t
-  val union : t -> t -> t
-  val rev_append : elt -> elt -> elt
-  val rev : elt -> elt
-  val xfold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> elt -> 'a1
-  val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1
-end
-
-val vars_of_pexpr : z pExpr -> Vars.t
-val vars_of_formula : z formula -> Vars.t
-val vars_of_bformula : (z formula, 'a1, 'a2, 'a3) gFormula -> Vars.t
 val bound_var : positive -> z formula
 val mk_eq_pos : positive -> positive -> positive -> z formula
-
-val bound_vars :
-     (positive -> positive -> bool option -> 'a2)
-  -> positive
-  -> Vars.t
-  -> (z formula, 'a1, 'a2, 'a3) gFormula
-
-val bound_problem_fr :
-     (positive -> positive -> bool option -> 'a2)
-  -> positive
-  -> (z formula, 'a1, 'a2, 'a3) gFormula
-  -> (z formula, 'a1, 'a2, 'a3) gFormula
-
+val max_var : positive -> z pol -> positive
+val max_var_nformulae : z nFormula list -> positive
 val zChecker : z nFormula list -> zArithProof -> bool
 val zTautoChecker : z formula bFormula -> zArithProof list -> bool
 
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index d92b409ba1..03f042647c 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -294,7 +294,7 @@ end
   *)
 
 module type Tag = sig
-  type t
+  type t = int
 
   val from : int -> t
   val next : t -> t
@@ -319,7 +319,9 @@ end
   * MODULE: Ordered sets of tags.
   *)
 
-module TagSet = Set.Make (Tag)
+module TagSet = struct
+  include Set.Make (Tag)
+end
 
 (** As for Unix.close_process, our Unix.waipid will ignore all EINTR *)
 
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index adf54713b9..a4f9b60b14 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -15,8 +15,7 @@
 (************************************************************************)
 
 open Num
-module Utils = Mutils
-open Utils
+open Mutils
 module Mc = Micromega
 
 let max_nb_cstr = ref max_int
@@ -43,6 +42,7 @@ module Monomial : sig
   val fold : (var -> int -> 'a -> 'a) -> t -> 'a -> 'a
   val sqrt : t -> t option
   val variables : t -> ISet.t
+  val degree : t -> int
 end = struct
   (* A monomial is represented by a multiset of variables  *)
   module Map = Map.Make (Int)
@@ -50,6 +50,8 @@ end = struct
 
   type t = int Map.t
 
+  let degree m = Map.fold (fun _ i d -> i + d) m 0
+
   let is_singleton m =
     try
       let k, v = choose m in
@@ -280,10 +282,11 @@ module LinPoly = struct
     let (monomial_of_index : Monomial.t IntMap.t ref) = ref IntMap.empty
     let fresh = ref 0
 
-    let clear () =
-      index_of_monomial := MonoMap.empty;
-      monomial_of_index := IntMap.empty;
-      fresh := 0
+    let reserve vr =
+      if !fresh > vr then failwith (Printf.sprintf "Cannot reserve %i" vr)
+      else fresh := vr + 1
+
+    let get_fresh () = !fresh
 
     let register m =
       try MonoMap.find m !index_of_monomial
@@ -295,6 +298,13 @@ module LinPoly = struct
         res
 
     let retrieve i = IntMap.find i !monomial_of_index
+
+    let clear () =
+      index_of_monomial := MonoMap.empty;
+      monomial_of_index := IntMap.empty;
+      fresh := 0;
+      ignore (register Monomial.const)
+
     let _ = register Monomial.const
   end
 
@@ -389,6 +399,11 @@ module LinPoly = struct
       (fun acc v _ -> ISet.union (Monomial.variables (MonT.retrieve v)) acc)
       ISet.empty p
 
+  let monomials p = Vect.fold (fun acc v _ -> ISet.add v acc) ISet.empty p
+
+  let degree v =
+    Vect.fold (fun acc v vl -> max acc (Monomial.degree (MonT.retrieve v))) 0 v
+
   let pp_goal typ o l =
     let vars =
       List.fold_left
@@ -433,6 +448,9 @@ module ProofFormat = struct
     | Done
     | Step of int * prf_rule * proof
     | Enum of int * prf_rule * Vect.t * prf_rule * proof list
+    | ExProof of int * int * int * var * var * var * proof
+
+  (* x = z - t, z >= 0, t >= 0 *)
 
   let rec output_prf_rule o = function
     | Annot (s, p) -> Printf.fprintf o "(%a)@%s" output_prf_rule p s
@@ -459,6 +477,9 @@ module ProofFormat = struct
     | Enum (i, p1, v, p2, pl) ->
       Printf.fprintf o "%i{%a<=%a<=%a}%a" i output_prf_rule p1 Vect.pp v
         output_prf_rule p2 (pp_list ";" output_proof) pl
+    | ExProof (i, j, k, x, z, t, pr) ->
+      Printf.fprintf o "%i := %i = %i - %i ; %i := %i >= 0 ; %i := %i >= 0 ; %a"
+        i x z t j z k t output_proof pr
 
   let rec pr_size = function
     | Annot (_, p) -> pr_size p
@@ -485,6 +506,8 @@ module ProofFormat = struct
     | Enum (i, p1, _, p2, l) ->
       let m = max (pr_rule_max_id p1) (pr_rule_max_id p2) in
       List.fold_left (fun i prf -> max i (proof_max_id prf)) (max i m) l
+    | ExProof (i, j, k, _, _, _, prf) ->
+      max (max (max i j) k) (proof_max_id prf)
 
   let rec pr_rule_def_cut id = function
     | Annot (_, p) -> pr_rule_def_cut id p
@@ -544,6 +567,16 @@ module ProofFormat = struct
             (ISet.union
                (ISet.union (pr_rule_collect_hyps p1) (pr_rule_collect_hyps p2))
                hyps) )
+      | ExProof (i, j, k, x, z, t, prf) ->
+        let prf', hyps = simplify_proof prf in
+        if
+          (not (ISet.mem i hyps))
+          && (not (ISet.mem j hyps))
+          && not (ISet.mem k hyps)
+        then (prf', hyps)
+        else
+          ( ExProof (i, j, k, x, z, t, prf')
+          , ISet.add i (ISet.add j (ISet.add k hyps)) )
     in
     fst (simplify_proof p)
 
@@ -561,6 +594,9 @@ module ProofFormat = struct
           bds
       in
       (id, prf)
+    | ExProof (i, j, k, x, z, t, prf) ->
+      let id, prf = normalise_proof id prf in
+      (id, ExProof (i, j, k, x, z, t, prf))
     | Enum (i, p1, v, p2, pl) ->
       (* Why do I have  top-level cuts ? *)
       (*      let p1 = implicit_cut p1 in
@@ -608,9 +644,9 @@ module ProofFormat = struct
     let rec compare p1 p2 =
       match (p1, p2) with
       | Annot (s1, p1), Annot (s2, p2) ->
-        if s1 = s2 then compare p1 p2 else Util.pervasives_compare s1 s2
-      | Hyp i, Hyp j -> Util.pervasives_compare i j
-      | Def i, Def j -> Util.pervasives_compare i j
+        if s1 = s2 then compare p1 p2 else String.compare s1 s2
+      | Hyp i, Hyp j -> Int.compare i j
+      | Def i, Def j -> Int.compare i j
       | Cst n, Cst m -> Num.compare_num n m
       | Zero, Zero -> 0
       | Square v1, Square v2 -> Vect.compare v1 v2
@@ -623,7 +659,7 @@ module ProofFormat = struct
       | AddPrf (p1, q1), MulPrf (p2, q2) ->
         cmp_pair compare compare (p1, q1) (p2, q2)
       | CutPrf p, CutPrf p' -> compare p p'
-      | _, _ -> Util.pervasives_compare (id_of_constr p1) (id_of_constr p2)
+      | _, _ -> Int.compare (id_of_constr p1) (id_of_constr p2)
   end
 
   let add_proof x y =
@@ -759,6 +795,8 @@ module ProofFormat = struct
         ( cmpl_prf_rule_z env p1
         , cmpl_prf_rule_z env p2
         , List.map (cmpl_proof (i :: env)) l )
+    | ExProof (i, j, k, x, _, _, prf) ->
+      Mc.ExProof (CamlToCoq.positive x, cmpl_proof (i :: j :: k :: env) prf)
 
   let compile_proof env prf =
     let id = 1 + proof_max_id prf in
@@ -818,6 +856,7 @@ module ProofFormat = struct
       let _ = eval_prf_rule (fun i -> IMap.find i env) r2 in
       (* Should check bounds *)
       failwith "Not implemented"
+    | ExProof _ -> failwith "Not implemented"
 end
 
 module WithProof = struct
@@ -852,7 +891,10 @@ module WithProof = struct
       let n, r = Vect.decomp_cst p in
       if Vect.is_null r && n >/ Int 0 then
         ((LinPoly.product p p1, o1), ProofFormat.mul_cst_proof n prf1)
-      else raise InvalidProof
+      else (
+        Printf.printf "mult_error %a [*] %a\n" LinPoly.pp p output
+          ((p1, o1), prf1);
+        raise InvalidProof )
 
   let cutting_plane ((p, o), prf) =
     let c, p' = Vect.decomp_cst p in
diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli
index e7c619affc..7e905ac69b 100644
--- a/plugins/micromega/polynomial.mli
+++ b/plugins/micromega/polynomial.mli
@@ -23,6 +23,9 @@ module Monomial : sig
   (** [fold f m acc]
        folds over the variables with multiplicities *)
 
+  val degree : t -> int
+  (** [degree m] is the sum of the degrees of each variable *)
+
   val const : t
   (** [const]
       @return the empty monomial i.e. without any variable *)
@@ -33,6 +36,10 @@ module Monomial : sig
   (** [var x]
       @return the monomial x^1 *)
 
+  val prod : t -> t -> t
+  (** [prod n m]
+      @return the monomial n*m *)
+
   val sqrt : t -> t option
   (** [sqrt m]
       @return [Some r] iff r^2 = m *)
@@ -142,6 +149,12 @@ module LinPoly : sig
     val clear : unit -> unit
     (** [clear ()] clears the mapping. *)
 
+    val reserve : int -> unit
+    (** [reserve i] reserves the integer i *)
+
+    val get_fresh : unit -> int
+    (** [get_fresh ()] return the first fresh variable *)
+
     val retrieve : int -> Monomial.t
     (** [retrieve x]
         @return the monomial corresponding to the variable [x] *)
@@ -225,6 +238,14 @@ module LinPoly : sig
       @return a mapping m such that m[s] = s^2
       for every s^2 that is a monomial of [p] *)
 
+  val monomials : t -> ISet.t
+  (** [monomials p]
+      @return the set of monomials. *)
+
+  val degree : t -> int
+  (** [degree p]
+      @return return the maximum degree *)
+
   val pp_var : out_channel -> var -> unit
   (** [pp_var o v] pretty-prints a monomial indexed by v. *)
 
@@ -260,6 +281,9 @@ module ProofFormat : sig
     | Done
     | Step of int * prf_rule * proof
     | Enum of int * prf_rule * Vect.t * prf_rule * proof list
+    | ExProof of int * int * int * var * var * var * proof
+
+  (* x = z - t, z >= 0, t >= 0 *)
 
   val pr_size : prf_rule -> Num.num
   val pr_rule_max_id : prf_rule -> int
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index 5bda268035..ade8143f3c 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -9,8 +9,6 @@
 (************************************************************************)
 
 open Polynomial
-(** A naive simplex *)
-
 open Num
 
 (*open Util*)
@@ -61,6 +59,12 @@ let output_tableau o t =
     (fun k v -> Printf.fprintf o "%a = %a\n" LinPoly.pp_var k pp_row v)
     t
 
+let output_env o t =
+  IMap.iter
+    (fun k v ->
+      Printf.fprintf o "%a : %a\n" LinPoly.pp_var k WithProof.output v)
+    t
+
 let output_vars o m =
   IMap.iter (fun k _ -> Printf.fprintf o "%a " LinPoly.pp_var k) m
 
@@ -329,16 +333,6 @@ open Mutils
 
 open Polynomial
 
-let fresh_var l =
-  1
-  +
-  try
-    ISet.max_elt
-      (List.fold_left
-         (fun acc c -> ISet.union acc (Vect.variables c.coeffs))
-         ISet.empty l)
-  with Not_found -> 0
-
 (*type varmap = (int * bool) IMap.t*)
 
 let make_certificate vm l =
@@ -349,6 +343,12 @@ let make_certificate vm l =
          Vect.set x' (if b then n else Num.minus_num n) acc)
        Vect.null l)
 
+(** [eliminate_equalities vr0 l]
+    represents an equality e = 0 of index idx in the list l
+    by 2 constraints (vr:e >= 0) and (vr+1:-e >= 0)
+    The mapping vm maps vr to idx
+ *)
+
 let eliminate_equalities (vr0 : var) (l : Polynomial.cstr list) =
   let rec elim idx vr vm l acc =
     match l with
@@ -374,6 +374,9 @@ let find_solution rst tbl =
       else Vect.set vr (Vect.get_cst v) res)
     tbl Vect.null
 
+let find_full_solution rst tbl =
+  IMap.fold (fun vr v res -> Vect.set vr (Vect.get_cst v) res) tbl Vect.null
+
 let choose_conflict (sol : Vect.t) (l : (var * Vect.t) list) =
   let esol = Vect.set 0 (Int 1) sol in
   let rec most_violating l e (x, v) rst =
@@ -404,12 +407,22 @@ let rec solve opt l (rst : Restricted.t) (t : tableau) =
     | Unsat c -> Inr c )
 
 let find_unsat_certificate (l : Polynomial.cstr list) =
-  let vr = fresh_var l in
+  let vr = LinPoly.MonT.get_fresh () in
   let _, vm, l' = eliminate_equalities vr l in
   match solve false l' (Restricted.make vr) IMap.empty with
   | Inr c -> Some (make_certificate vm c)
   | Inl _ -> None
 
+let fresh_var l =
+  1
+  +
+  try
+    ISet.max_elt
+      (List.fold_left
+         (fun acc c -> ISet.union acc (Vect.variables c.coeffs))
+         ISet.empty l)
+  with Not_found -> 0
+
 let find_point (l : Polynomial.cstr list) =
   let vr = fresh_var l in
   let _, vm, l' = eliminate_equalities vr l in
@@ -418,7 +431,7 @@ let find_point (l : Polynomial.cstr list) =
   | _ -> None
 
 let optimise obj l =
-  let vr0 = fresh_var l in
+  let vr0 = LinPoly.MonT.get_fresh () in
   let _, vm, l' = eliminate_equalities (vr0 + 1) l in
   let bound pos res =
     match res with
@@ -471,43 +484,17 @@ let make_farkas_proof (env : WithProof.t IMap.t) vm v =
 
 let frac_num n = n -/ Num.floor_num n
 
-(* [resolv_var v rst tbl] returns (if it exists) a restricted variable vr such that v = vr *)
-exception FoundVar of int
-
-let resolve_var v rst tbl =
-  let v = Vect.set v (Int 1) Vect.null in
-  try
-    IMap.iter
-      (fun k vect ->
-        if Restricted.is_restricted k rst then
-          if Vect.equal v vect then raise (FoundVar k) else ())
-      tbl;
-    None
-  with FoundVar k -> Some k
-
-let prepare_cut env rst tbl x v =
-  (* extract the unrestricted part *)
-  let unrst, rstv =
-    Vect.partition
-      (fun x vl ->
-        (not (Restricted.is_restricted x rst)) && frac_num vl <>/ Int 0)
-      (Vect.set 0 (Int 0) v)
-  in
-  if Vect.is_null unrst then Some rstv
-  else
-    Some
-      (Vect.fold
-         (fun acc k i ->
-           match resolve_var k rst tbl with
-           | None -> acc (* Should not happen *)
-           | Some v' -> Vect.set v' i acc)
-         rstv unrst)
+type ('a, 'b) hitkind =
+  | Forget
+  (* Not interesting *)
+  | Hit of 'a
+  (* Yes, we have a positive result *)
+  | Keep of 'b
 
 let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) =
-  (*    Printf.printf "Trying to cut %i\n" x;*)
   let n, r = Vect.decomp_cst v in
   let f = frac_num n in
-  if f =/ Int 0 then None (* The solution is integral *)
+  if f =/ Int 0 then Forget (* The solution is integral *)
   else
     (* This is potentially a cut *)
     let t =
@@ -522,11 +509,11 @@ let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) =
     in
     let cut_coeff2 v = frac_num (t */ v) in
     let cut_vector ccoeff =
-      match prepare_cut env rst tbl x v with
-      | None -> Vect.null
-      | Some r ->
-        (*Printf.printf "Potential cut %a\n" LinPoly.pp r;*)
-        Vect.fold (fun acc x n -> Vect.set x (ccoeff n) acc) Vect.null r
+      Vect.fold
+        (fun acc x n ->
+          if Restricted.is_restricted x rst then Vect.set x (ccoeff n) acc
+          else acc)
+        Vect.null r
     in
     let lcut =
       List.map
@@ -538,52 +525,100 @@ let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) =
       match WithProof.cutting_plane c with
       | None ->
         if debug then
-          Printf.printf "This is not cutting plane for %a\n%a:" LinPoly.pp_var x
-            WithProof.output c;
+          Printf.printf "This is not a cutting plane for %a\n%a:" LinPoly.pp_var
+            x WithProof.output c;
         None
       | Some (v, prf) ->
-        if debug then begin
+        if debug then (
           Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x;
-          Printf.printf " %a\n" WithProof.output (v, prf)
-        end;
+          Printf.printf " %a\n" WithProof.output (v, prf) );
         if snd v = Eq then (* Unsat *) Some (x, (v, prf))
         else
           let vl = Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol) in
-          if eval_op Ge vl (Int 0) then begin
-            (* Can this happen? *)
+          if eval_op Ge vl (Int 0) then (
             if debug then
-              Printf.printf "The cut is feasible %s >= 0 ??\n"
+              Printf.printf "The cut is feasible %s >= 0 \n"
                 (Num.string_of_num vl);
-            None
-          end
+            None )
           else Some (x, (v, prf))
     in
-    find_some check_cutting_plane lcut
+    match find_some check_cutting_plane lcut with
+    | Some r -> Hit r
+    | None -> Keep (x, v)
+
+let merge_result_old oldr f x =
+  match oldr with
+  | Hit v -> Hit v
+  | Forget -> (
+    match f x with Forget -> Forget | Hit v -> Hit v | Keep v -> Keep v )
+  | Keep v -> (
+    match f x with Forget -> Keep v | Keep v' -> Keep v | Hit v -> Hit v )
+
+let merge_best lt oldr newr =
+  match (oldr, newr) with
+  | x, Forget -> x
+  | Hit v, Hit v' -> if lt v v' then Hit v else Hit v'
+  | _, Hit v | Hit v, _ -> Hit v
+  | Forget, Keep v -> Keep v
+  | Keep v, Keep v' -> Keep v'
 
 let find_cut nb env u sol vm rst tbl =
   if nb = 0 then
     IMap.fold
-      (fun x v acc ->
-        match acc with
-        | None -> cut env u sol vm rst tbl (x, v)
-        | Some c -> Some c)
-      tbl None
+      (fun x v acc -> merge_result_old acc (cut env u sol vm rst tbl) (x, v))
+      tbl Forget
   else
+    let lt (_, (_, p1)) (_, (_, p2)) =
+      ProofFormat.pr_size p1 </ ProofFormat.pr_size p2
+    in
     IMap.fold
-      (fun x v acc ->
-        match (cut env u sol vm rst tbl (x, v), acc) with
-        | None, Some r | Some r, None -> Some r
-        | None, None -> None
-        | Some (v, ((lp, o), p1)), Some (v', ((lp', o'), p2)) ->
-          Some
-            ( if ProofFormat.pr_size p1 </ ProofFormat.pr_size p2 then
-              (v, ((lp, o), p1))
-            else (v', ((lp', o'), p2)) ))
-      tbl None
+      (fun x v acc -> merge_best lt acc (cut env u sol vm rst tbl (x, v)))
+      tbl Forget
+
+let var_of_vect v = fst (fst (Vect.decomp_fst v))
+
+let eliminate_variable (bounded, vr, env, tbl) x =
+  if debug then
+    Printf.printf "Eliminating variable %a from tableau\n%a\n" LinPoly.pp_var x
+      output_tableau tbl;
+  (* We identify the new variables with the constraint. *)
+  LinPoly.MonT.reserve vr;
+  let z = LinPoly.var (vr + 1) in
+  let zv = var_of_vect z in
+  let t = LinPoly.var (vr + 2) in
+  let tv = var_of_vect t in
+  (* x = z - t *)
+  let xdef = Vect.add z (Vect.uminus t) in
+  let xp = ((Vect.set x (Int 1) (Vect.uminus xdef), Eq), Def vr) in
+  let zp = ((z, Ge), Def zv) in
+  let tp = ((t, Ge), Def tv) in
+  (* Pivot the current tableau using xdef *)
+  let tbl = IMap.map (fun v -> Vect.subst x xdef v) tbl in
+  (* Pivot the environment *)
+  let env =
+    IMap.map
+      (fun lp ->
+        let (v, o), p = lp in
+        let ai = Vect.get x v in
+        if ai =/ Int 0 then lp
+        else
+          WithProof.addition
+            (WithProof.mult (Vect.cst (Num.minus_num ai)) xp)
+            lp)
+      env
+  in
+  (* Add the variables to the environment *)
+  let env = IMap.add vr xp (IMap.add zv zp (IMap.add tv tp env)) in
+  (* Remember the mapping *)
+  let bounded = IMap.add x (vr, zv, tv) bounded in
+  if debug then (
+    Printf.printf "Tableau without\n %a\n" output_tableau tbl;
+    Printf.printf "Environment\n %a\n" output_env env );
+  (bounded, vr + 3, env, tbl)
 
 let integer_solver lp =
   let l, _ = List.split lp in
-  let vr0 = fresh_var l in
+  let vr0 = 3 * LinPoly.MonT.get_fresh () in
   let vr, vm, l' = eliminate_equalities vr0 l in
   let _, env = env_of_list (List.map WithProof.of_cstr lp) in
   let insert_row vr v rst tbl =
@@ -601,24 +636,46 @@ let integer_solver lp =
       if debug then begin
         Printf.fprintf stdout "Looking for a cut\n";
         Printf.fprintf stdout "Restricted %a ...\n" Restricted.pp rst;
-        Printf.fprintf stdout "Current Tableau\n%a\n" output_tableau tbl
+        Printf.fprintf stdout "Current Tableau\n%a\n" output_tableau tbl;
+        flush stdout
         (*           Printf.fprintf stdout "Bounding box\n%a\n" output_box (bounding_box (vr+1) rst tbl l')*)
       end;
-      let sol = find_solution rst tbl in
+      let sol = find_full_solution rst tbl in
       match find_cut (!nb mod 2) env cr (*x*) sol vm rst tbl with
-      | None -> None
-      | Some (cr, ((v, op), cut)) -> (
+      | Forget ->
+        None (* There is no hope, there should be an integer solution *)
+      | Hit (cr, ((v, op), cut)) ->
         if op = Eq then
           (* This is a contradiction *)
           Some (Step (vr, CutPrf cut, Done))
-        else
+        else (
+          LinPoly.MonT.reserve vr;
           let res = insert_row vr v (Restricted.set_exc vr rst) tbl in
           let prf =
             isolve (IMap.add vr ((v, op), Def vr) env) (Some cr) (vr + 1) res
           in
           match prf with
           | None -> None
-          | Some p -> Some (Step (vr, CutPrf cut, p)) ) )
+          | Some p -> Some (Step (vr, CutPrf cut, p)) )
+      | Keep (x, v) -> (
+        if debug then
+          Printf.fprintf stdout "Remove %a from Tableau\n" LinPoly.pp_var x;
+        let bounded, vr, env, tbl =
+          Vect.fold
+            (fun acc x n ->
+              if x <> 0 && not (Restricted.is_restricted x rst) then
+                eliminate_variable acc x
+              else acc)
+            (IMap.empty, vr, env, tbl) v
+        in
+        let prf = isolve env cr vr (Inl (rst, tbl, None)) in
+        match prf with
+        | None -> None
+        | Some pf ->
+          Some
+            (IMap.fold
+               (fun x (vr, zv, tv) acc -> ExProof (vr, zv, tv, x, zv, tv, acc))
+               bounded pf) ) )
   in
   let res = solve true l' (Restricted.make vr0) IMap.empty in
   isolve env None vr res
diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml
index 581dc79cef..f53a7b42c9 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -19,6 +19,7 @@ type var = int
  *)
 
 type t = (var * num) list
+type vector = t
 
 (** [equal v1 v2 = true] if the vectors are syntactically equal. *)
 
@@ -134,7 +135,7 @@ let rec add (ve1 : t) (ve2 : t) =
   match (ve1, ve2) with
   | [], v | v, [] -> v
   | (v1, c1) :: l1, (v2, c2) :: l2 ->
-    let cmp = Util.pervasives_compare v1 v2 in
+    let cmp = Int.compare v1 v2 in
     if cmp == 0 then
       let s = add_num c1 c2 in
       if eq_num (Int 0) s then add l1 l2 else (v1, s) :: add l1 l2
@@ -146,7 +147,7 @@ let rec xmul_add (n1 : num) (ve1 : t) (n2 : num) (ve2 : t) =
   | [], _ -> mul n2 ve2
   | _, [] -> mul n1 ve1
   | (v1, c1) :: l1, (v2, c2) :: l2 ->
-    let cmp = Util.pervasives_compare v1 v2 in
+    let cmp = Int.compare v1 v2 in
     if cmp == 0 then
       let s = (n1 */ c1) +/ (n2 */ c2) in
       if eq_num (Int 0) s then xmul_add n1 l1 n2 l2
@@ -195,6 +196,17 @@ let rec decomp_at i v =
     if i = vr then (vl, r) else if i < vr then (Int 0, v) else decomp_at i r
 
 let decomp_fst v = match v with [] -> ((0, Int 0), []) | x :: v -> (x, v)
+
+let rec subst (vr : int) (e : t) (v : t) =
+  match v with
+  | [] -> []
+  | (x, n) :: v' -> (
+    match Int.compare vr x with
+    | 0 -> mul_add n e (Int 1) v'
+    | -1 -> v
+    | 1 -> add [(x, n)] (subst vr e v')
+    | _ -> assert false )
+
 let fold f acc v = List.fold_left (fun acc (v, i) -> f acc v i) acc v
 
 let fold_error f acc v =
@@ -269,3 +281,13 @@ let abs_min_elt v =
 
 let partition p = List.partition (fun (vr, vl) -> p vr vl)
 let mkvar x = set x (Int 1) null
+
+module Bound = struct
+  type t = {cst : num; var : var; coeff : num}
+
+  let of_vect (v : vector) =
+    match v with
+    | [(x, v)] -> if x = 0 then None else Some {cst = Int 0; var = x; coeff = v}
+    | [(0, v); (x, v')] -> Some {cst = v; var = x; coeff = v'}
+    | _ -> None
+end
diff --git a/plugins/micromega/vect.mli b/plugins/micromega/vect.mli
index 83d9ef32b0..4b814cbb82 100644
--- a/plugins/micromega/vect.mli
+++ b/plugins/micromega/vect.mli
@@ -25,6 +25,8 @@ type t
            are not represented.
         *)
 
+type vector = t
+
 (** {1 Generic functions}  *)
 
 (** [hash] [equal] and [compare] so that Vect.t can be used as
@@ -135,6 +137,9 @@ val mul : num -> t -> t
 val mul_add : num -> t -> num -> t -> t
 (** [mul_add c1 v1 c2 v2] returns the linear combination c1.v1+c2.v2 *)
 
+val subst : int -> t -> t -> t
+(** [subst x v v'] replaces x by v in vector v' *)
+
 val div : num -> t -> t
 (** [div c1 v1] returns the mutiplication by the inverse of c1 i.e (1/c1).v1 *)
 
@@ -170,3 +175,10 @@ val dotproduct : t -> t -> num
 val map : (var -> num -> 'a) -> t -> 'a list
 val abs_min_elt : t -> (var * num) option
 val partition : (var -> num -> bool) -> t -> t * t
+
+module Bound : sig
+  type t = {cst : num; var : var; coeff : num}
+  (** represents a0 + ai.xi  *)
+
+  val of_vect : vector -> t option
+end
diff --git a/test-suite/micromega/bug_11270.v b/test-suite/micromega/bug_11270.v
new file mode 100644
index 0000000000..80abc6d0e9
--- /dev/null
+++ b/test-suite/micromega/bug_11270.v
@@ -0,0 +1,6 @@
+Require Import Psatz.
+Theorem foo : forall a b, 1 <= S (a + a * S b).
+Proof.
+intros.
+lia.
+Qed.
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index 668be1fdbc..357afb51eb 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -56,10 +56,11 @@ Extract Constant Rinv   => "fun x -> 1 / x".
 Recursive Extraction
            Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
            Tauto.abst_form
-           ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ
+           ZMicromega.cnfZ  ZMicromega.Zeval_const QMicromega.cnfQ
            List.map simpl_cone (*map_cone  indexes*)
            denorm Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+
 (* Local Variables: *)
 (* coding: utf-8 *)
 (* End: *)
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 303acf7ae2..e3ff4979a9 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -18,6 +18,8 @@
     [equal s s'=true] instead of [Equal s s'], etc. *)
 
 Require Import MSetProperties Zerob Sumbool Lia DecidableTypeEx.
+Require  FSetEqProperties.
+
 
 Module WEqPropertiesOn (Import E:DecidableType)(M:WSetsOn E).
 Module Import MP := WPropertiesOn E M.
@@ -857,7 +859,7 @@ intros.
 rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H).
 rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H).
 rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto.
-intros. do 3 (rewrite fold_add; auto with fset). lia.
+intros. do 3 (rewrite fold_add by auto with fset). lia.
 do 3 rewrite fold_empty;auto.
 Qed.
 
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 5b3d6ea30e..b1f0d9bc39 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Export Rbase.
+Require Import Rdefinitions Raxioms RIneq.
 Require Export QArith_base.
 
 (** Injection of rational numbers into real numbers. *)
@@ -48,7 +48,7 @@ set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2);
  set (Y2 := IZR (Zpos y2)) in *.
 assert ((X1 * Y2)%R = (Y1 * X2)%R).
  unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR.
- apply IZR_eq; auto.
+f_equal; auto.
 clear H.
 field_simplify_eq; auto.
 rewrite H0; ring.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index cbf90c5adb..0cad621692 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Rbase.
+Require Import Rdefinitions Raxioms RIneq.
 Require Import Rbasic_fun.
 Require Import Even.
 Require Import Div2.
@@ -85,7 +85,7 @@ Proof.
   assert (H1 := le_INR _ _ H).
   do 2 rewrite mult_INR in H1.
   apply Rmult_le_reg_l with (INR 2).
-  replace (INR 2) with 2; [ prove_sup0 | reflexivity ].
+  apply lt_0_INR. apply Nat.lt_0_2.
   assumption.
 Qed.
 
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 229e6018ca..b0d7b26a86 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -19,7 +19,7 @@ Require Export Raxioms.
 Require Import Rpow_def.
 Require Import Zpower.
 Require Export ZArithRing.
-Require Import Lia.
+Require Import Ztac.
 Require Export RealField.
 
 Local Open Scope Z_scope.
@@ -1875,7 +1875,7 @@ Lemma eq_IZR : forall n m:Z, IZR n = IZR m -> n = m.
 Proof.
   intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H);
     rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0);
-      intro; lia.
+      apply Zminus_eq.
 Qed.
 
 (**********)
@@ -1913,21 +1913,24 @@ Qed.
 Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m.
 Proof.
   intros m n H; apply Rnot_lt_ge; red; intro.
-  generalize (lt_IZR m n H0); intro; lia.
+  generalize (lt_IZR m n H0); intro.
+  slia H H1.
 Qed.
 
 Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m.
 Proof.
   intros m n H; apply Rnot_gt_le; red; intro.
-  unfold Rgt in H0; generalize (lt_IZR n m H0); intro; lia.
+  unfold Rgt in H0; generalize (lt_IZR n m H0); intro.
+  slia H H1.
 Qed.
 
 Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.
 Proof.
   intros m n H; cut (m <= n)%Z.
   intro H0; elim (IZR_le m n H0); intro; auto.
-  generalize (eq_IZR m n H1); intro; exfalso; lia.
-  lia.
+  generalize (eq_IZR m n H1); intro; exfalso.
+  slia H H3.
+  normZ. slia H H0.
 Qed.
 
 Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2.
@@ -1954,7 +1957,7 @@ Lemma one_IZR_r_R1 :
   forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m.
 Proof.
   intros r z x [H1 H2] [H3 H4].
-  cut ((z - x)%Z = 0%Z). lia.
+  apply Zminus_eq.
   apply one_IZR_lt1.
   rewrite <- Z_R_minus; split.
   replace (-1) with (r - (r + 1)).
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 5f0747d869..d9820f9444 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -13,8 +13,8 @@
 (*                                                        *)
 (**********************************************************)
 
-Require Import Rbase.
-Require Import Lia.
+Require Import Rdefinitions Raxioms RIneq.
+Require Import Ztac.
 Local Open Scope R_scope.
 
 (*********************************************************)
@@ -60,7 +60,7 @@ Proof.
   apply lt_IZR in H1.
   rewrite <- minus_IZR in H2.
   apply le_IZR in H2.
-  lia.
+  normZ. slia H2 HZ. slia H1 HZ.
 Qed.
 
 (**********)
@@ -229,8 +229,8 @@ Proof.
                                                                                                                     rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H.
     rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H;
       generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H);
-        intros; clear H H0; unfold Int_part at 1;
-          lia.
+        intros; clear H H0; unfold Int_part at 1.
+    normZ. slia H HZ. slia H0 HZ.
 Qed.
 
 (**********)
@@ -322,8 +322,8 @@ Proof.
           generalize (Rlt_le (IZR (Int_part r1 - Int_part r2 - 1)) (r1 - r2) H);
             intro; clear H;
               generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2 - 1) H1 H0);
-                intros; clear H0 H1; unfold Int_part at 1;
-                  lia.
+                intros; clear H0 H1; unfold Int_part at 1.
+  normZ.  slia H HZ. slia H0 HZ.
 Qed.
 
 (**********)
@@ -437,7 +437,8 @@ Proof.
           rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H0;
             rewrite <- (plus_IZR (Int_part r1 + Int_part r2 + 1) 1) in H0;
               generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2 + 1) H H0);
-                intro; clear H H0; unfold Int_part at 1; lia.
+              intro; clear H H0; unfold Int_part at 1.
+    normZ. slia H HZ. slia H0 HZ.
 Qed.
 
 (**********)
@@ -498,8 +499,8 @@ Proof.
       rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1;
         rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1;
           generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1);
-            intro; clear H0 H1; unfold Int_part at 1;
-              lia.
+            intro; clear H0 H1; unfold Int_part at 1.
+    normZ. slia H HZ. slia H0 HZ.
 Qed.
 
 (**********)
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 1a74582b71..e6c6e8bf48 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Rbase.
+Require Import Rdefinitions Raxioms RIneq.
 Require Import Rbasic_fun.
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index efca826077..7e59639dd4 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -13,7 +13,7 @@
 (*                                                       *)
 (*********************************************************)
 
-Require Import Rbase.
+Require Import Rdefinitions Raxioms RIneq.
 Require Import R_Ifp.
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 7f9e019c5b..a63df38808 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -17,7 +17,7 @@
 (********************************************************)
 Require Export ArithRing.
 
-Require Import Rbase.
+Require Import Rdefinitions Raxioms RIneq.
 Require Export Rpow_def.
 Require Export R_Ifp.
 Require Export Rbasic_fun.
@@ -25,8 +25,8 @@ Require Export R_sqr.
 Require Export SplitAbsolu.
 Require Export SplitRmult.
 Require Export ArithProp.
-Require Import Lia.
 Require Import Zpower.
+Require Import Ztac.
 Local Open Scope nat_scope.
 Local Open Scope R_scope.
 
@@ -122,7 +122,7 @@ Hint Resolve pow_lt: real.
 Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
 Proof.
   intros x n; elim n; simpl; auto with real.
-  intros H' H'0; exfalso; lia.
+  intros H' H'0; exfalso. apply (Nat.lt_irrefl 0); assumption.
   intros n0; case n0.
   simpl; rewrite Rmult_1_r; auto.
   intros n1 H' H'0 H'1.
@@ -262,14 +262,14 @@ Proof.
   elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0;
     apply
       (Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
-  rewrite INR_IZR_INZ; apply IZR_ge; lia.
+  rewrite INR_IZR_INZ; apply IZR_ge. normZ. slia H3 H5.
   unfold Rge; left; assumption.
   exists 0%nat;
     apply
       (Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
-  rewrite INR_IZR_INZ; apply IZR_ge; simpl; lia.
+  rewrite INR_IZR_INZ; apply IZR_ge; simpl. normZ. slia H2 H3.
   unfold Rge; left; assumption.
-  lia.
+  apply Z.le_ge_cases.
 Qed.
 
 Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0.
@@ -745,7 +745,8 @@ Proof.
   - now simpl; rewrite Rmult_1_l.
   - now rewrite <- !pow_powerRZ, Rpow_mult_distr.
   - destruct Hmxy as [H|H].
-    + assert(m = 0) as -> by now lia.
+    + assert(m = 0) as -> by
+      (destruct n; [assumption| subst; simpl in H; lia_contr]).
       now rewrite <- Hm, Rmult_1_l.
     + assert(x0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_l.
       assert(y0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_r.
@@ -808,7 +809,7 @@ Proof.
   ring.
   rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n).
   intro H; rewrite H; simpl; ring.
-  lia.
+  apply Nat.add_1_r.
 Qed.
 
 Lemma sum_f_R0_triangle :
diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v
index be2b5a73f3..cad1525580 100644
--- a/theories/Reals/SplitRmult.v
+++ b/theories/Reals/SplitRmult.v
@@ -11,7 +11,7 @@
 (*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*)
 
 
-Require Import Rbase.
+Require Import Rdefinitions Raxioms RIneq.
 
 Ltac split_Rmult :=
   match goal with