Goal:
  
  __p1 : Prop
  __x7 : BinNums.Z
  __x6 : BinNums.Z
  __x5 : BinNums.Z
  __x4 : BinNums.Z
  __x3 : BinNums.Z
  __x2 : BinNums.Z
  __x1 : BinNums.Z
  __wit := [ZMicromega.RatProof
              (RingMicromega.PsatzAdd
                 (RingMicromega.PsatzMulC
                    (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                    (RingMicromega.PsatzIn BinNums.Z 7))
                 (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 3)
                    (RingMicromega.PsatzIn BinNums.Z 0)))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 7)
                 (RingMicromega.PsatzAdd
                    (RingMicromega.PsatzMulC
                       (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                       (RingMicromega.PsatzIn BinNums.Z 3))
                    (RingMicromega.PsatzIn BinNums.Z 0)))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 7)
                 (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 4)
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzMulC
                          (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                          (RingMicromega.PsatzIn BinNums.Z 3))
                       (RingMicromega.PsatzIn BinNums.Z 0))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 8)
                 (RingMicromega.PsatzAdd
                    (RingMicromega.PsatzMulC
                       (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                       (RingMicromega.PsatzIn BinNums.Z 7))
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzIn BinNums.Z 6)
                       (RingMicromega.PsatzAdd
                          (RingMicromega.PsatzMulC
                             (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                             (RingMicromega.PsatzIn BinNums.Z 5))
                          (RingMicromega.PsatzAdd
                             (RingMicromega.PsatzIn BinNums.Z 3)
                             (RingMicromega.PsatzIn BinNums.Z 0))))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 7)
                 (RingMicromega.PsatzAdd
                    (RingMicromega.PsatzMulC
                       (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                       (RingMicromega.PsatzIn BinNums.Z 6))
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzMulC
                          (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                          (RingMicromega.PsatzIn BinNums.Z 5))
                       (RingMicromega.PsatzAdd
                          (RingMicromega.PsatzIn BinNums.Z 3)
                          (RingMicromega.PsatzIn BinNums.Z 0)))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 6)
                 (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 4)
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzMulC
                          (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                          (RingMicromega.PsatzIn BinNums.Z 3))
                       (RingMicromega.PsatzIn BinNums.Z 0))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 6)
                 (RingMicromega.PsatzAdd
                    (RingMicromega.PsatzMulC
                       (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                       (RingMicromega.PsatzIn BinNums.Z 3))
                    (RingMicromega.PsatzIn BinNums.Z 0)))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd
                 (RingMicromega.PsatzMulC
                    (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                    (RingMicromega.PsatzIn BinNums.Z 6))
                 (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 3)
                    (RingMicromega.PsatzIn BinNums.Z 0)))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 7)
                 (RingMicromega.PsatzAdd
                    (RingMicromega.PsatzMulC
                       (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                       (RingMicromega.PsatzIn BinNums.Z 6))
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzIn BinNums.Z 3)
                       (RingMicromega.PsatzIn BinNums.Z 0))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 6)
                 (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 5)
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzIn BinNums.Z 4)
                       (RingMicromega.PsatzAdd
                          (RingMicromega.PsatzMulC
                             (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                             (RingMicromega.PsatzIn BinNums.Z 3))
                          (RingMicromega.PsatzIn BinNums.Z 0)))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 6)
                 (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 5)
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzMulC
                          (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                          (RingMicromega.PsatzIn BinNums.Z 3))
                       (RingMicromega.PsatzIn BinNums.Z 0))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd
                 (RingMicromega.PsatzMulC
                    (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                    (RingMicromega.PsatzIn BinNums.Z 6))
                 (RingMicromega.PsatzAdd
                    (RingMicromega.PsatzMulC
                       (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                       (RingMicromega.PsatzIn BinNums.Z 5))
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzIn BinNums.Z 3)
                       (RingMicromega.PsatzIn BinNums.Z 0))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd
                 (RingMicromega.PsatzMulC
                    (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                    (RingMicromega.PsatzIn BinNums.Z 7))
                 (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 6)
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzMulC
                          (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                          (RingMicromega.PsatzIn BinNums.Z 5))
                       (RingMicromega.PsatzAdd
                          (RingMicromega.PsatzIn BinNums.Z 3)
                          (RingMicromega.PsatzIn BinNums.Z 0)))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 7)
                 (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 5)
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzMulC
                          (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                          (RingMicromega.PsatzIn BinNums.Z 3))
                       (RingMicromega.PsatzAdd
                          (RingMicromega.PsatzIn BinNums.Z 2)
                          (RingMicromega.PsatzAdd
                             (RingMicromega.PsatzIn BinNums.Z 1)
                             (RingMicromega.PsatzIn BinNums.Z 0))))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 7)
                 (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 5)
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzIn BinNums.Z 4)
                       (RingMicromega.PsatzAdd
                          (RingMicromega.PsatzMulC
                             (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                             (RingMicromega.PsatzIn BinNums.Z 3))
                          (RingMicromega.PsatzAdd
                             (RingMicromega.PsatzIn BinNums.Z 2)
                             (RingMicromega.PsatzAdd
                                (RingMicromega.PsatzIn BinNums.Z 1)
                                (RingMicromega.PsatzIn BinNums.Z 0)))))))
              ZMicromega.DoneProof;
            ZMicromega.RatProof
              (RingMicromega.PsatzAdd (RingMicromega.PsatzIn BinNums.Z 8)
                 (RingMicromega.PsatzAdd
                    (RingMicromega.PsatzMulC
                       (EnvRing.Pc (BinNums.Zneg BinNums.xH))
                       (RingMicromega.PsatzIn BinNums.Z 7))
                    (RingMicromega.PsatzAdd
                       (RingMicromega.PsatzIn BinNums.Z 3)
                       (RingMicromega.PsatzIn BinNums.Z 0))))
              ZMicromega.DoneProof] : list ZMicromega.ZArithProof
  __varmap := VarMap.Branch
                (VarMap.Branch (VarMap.Elt __x4) __x2 (VarMap.Elt __x6)) __x1
                (VarMap.Branch (VarMap.Elt __x5) __x3 (VarMap.Elt __x7))
           : VarMap.t BinNums.Z
  __ff := Tauto.IMPL
            (Tauto.OR
               (Tauto.AND
                  (Tauto.A Tauto.isProp
                     {|
                       RingMicromega.Flhs := EnvRing.PEc BinNums.Z0;
                       RingMicromega.Fop := RingMicromega.OpLt;
                       RingMicromega.Frhs :=
                         EnvRing.PEsub
                           (EnvRing.PEadd
                              (EnvRing.PEX
                                 (BinNums.xI (BinNums.xI BinNums.xH)))
                              (EnvRing.PEX
                                 (BinNums.xO (BinNums.xI BinNums.xH))))
                           (EnvRing.PEX (BinNums.xI BinNums.xH))
                     |} tt)
                  (Tauto.A Tauto.isProp
                     {|
                       RingMicromega.Flhs := EnvRing.PEX BinNums.xH;
                       RingMicromega.Fop := RingMicromega.OpEq;
                       RingMicromega.Frhs :=
                         EnvRing.PEsub
                           (EnvRing.PEadd
                              (EnvRing.PEX
                                 (BinNums.xI (BinNums.xI BinNums.xH)))
                              (EnvRing.PEX
                                 (BinNums.xO (BinNums.xI BinNums.xH))))
                           (EnvRing.PEX (BinNums.xI BinNums.xH))
                     |} tt))
               (Tauto.AND
                  (Tauto.A Tauto.isProp
                     {|
                       RingMicromega.Flhs :=
                         EnvRing.PEsub
                           (EnvRing.PEadd
                              (EnvRing.PEX
                                 (BinNums.xI (BinNums.xI BinNums.xH)))
                              (EnvRing.PEX
                                 (BinNums.xO (BinNums.xI BinNums.xH))))
                           (EnvRing.PEX (BinNums.xI BinNums.xH));
                       RingMicromega.Fop := RingMicromega.OpLe;
                       RingMicromega.Frhs := EnvRing.PEc BinNums.Z0
                     |} tt)
                  (Tauto.A Tauto.isProp
                     {|
                       RingMicromega.Flhs := EnvRing.PEX BinNums.xH;
                       RingMicromega.Fop := RingMicromega.OpEq;
                       RingMicromega.Frhs := EnvRing.PEc BinNums.Z0
                     |} tt))) None
            (Tauto.IMPL
               (Tauto.OR
                  (Tauto.AND (Tauto.X Tauto.isProp __p1)
                     (Tauto.A Tauto.isProp
                        {|
                          RingMicromega.Flhs :=
                            EnvRing.PEX (BinNums.xI (BinNums.xI BinNums.xH));
                          RingMicromega.Fop := RingMicromega.OpEq;
                          RingMicromega.Frhs :=
                            EnvRing.PEsub
                              (EnvRing.PEX
                                 (BinNums.xO (BinNums.xO BinNums.xH)))
                              (EnvRing.PEc (BinNums.Zpos BinNums.xH))
                        |} tt))
                  (Tauto.AND
                     (Tauto.A Tauto.isProp
                        {|
                          RingMicromega.Flhs :=
                            EnvRing.PEsub
                              (EnvRing.PEX
                                 (BinNums.xO (BinNums.xO BinNums.xH)))
                              (EnvRing.PEc (BinNums.Zpos BinNums.xH));
                          RingMicromega.Fop := RingMicromega.OpLe;
                          RingMicromega.Frhs := EnvRing.PEc BinNums.Z0
                        |} tt)
                     (Tauto.A Tauto.isProp
                        {|
                          RingMicromega.Flhs :=
                            EnvRing.PEX (BinNums.xI (BinNums.xI BinNums.xH));
                          RingMicromega.Fop := RingMicromega.OpEq;
                          RingMicromega.Frhs := EnvRing.PEc BinNums.Z0
                        |} tt))) None
               (Tauto.IMPL
                  (Tauto.OR
                     (Tauto.AND
                        (Tauto.A Tauto.isProp
                           {|
                             RingMicromega.Flhs := EnvRing.PEc BinNums.Z0;
                             RingMicromega.Fop := RingMicromega.OpLt;
                             RingMicromega.Frhs :=
                               EnvRing.PEsub
                                 (EnvRing.PEadd
                                    (EnvRing.PEX
                                       (BinNums.xO (BinNums.xO BinNums.xH)))
                                    (EnvRing.PEX
                                       (BinNums.xO (BinNums.xI BinNums.xH))))
                                 (EnvRing.PEadd
                                    (EnvRing.PEX (BinNums.xI BinNums.xH))
                                    (EnvRing.PEc (BinNums.Zpos BinNums.xH)))
                           |} tt)
                        (Tauto.A Tauto.isProp
                           {|
                             RingMicromega.Flhs :=
                               EnvRing.PEX (BinNums.xO BinNums.xH);
                             RingMicromega.Fop := RingMicromega.OpEq;
                             RingMicromega.Frhs :=
                               EnvRing.PEsub
                                 (EnvRing.PEadd
                                    (EnvRing.PEX
                                       (BinNums.xO (BinNums.xO BinNums.xH)))
                                    (EnvRing.PEX
                                       (BinNums.xO (BinNums.xI BinNums.xH))))
                                 (EnvRing.PEadd
                                    (EnvRing.PEX (BinNums.xI BinNums.xH))
                                    (EnvRing.PEc (BinNums.Zpos BinNums.xH)))
                           |} tt))
                     (Tauto.AND
                        (Tauto.A Tauto.isProp
                           {|
                             RingMicromega.Flhs :=
                               EnvRing.PEsub
                                 (EnvRing.PEadd
                                    (EnvRing.PEX
                                       (BinNums.xO (BinNums.xO BinNums.xH)))
                                    (EnvRing.PEX
                                       (BinNums.xO (BinNums.xI BinNums.xH))))
                                 (EnvRing.PEadd
                                    (EnvRing.PEX (BinNums.xI BinNums.xH))
                                    (EnvRing.PEc (BinNums.Zpos BinNums.xH)));
                             RingMicromega.Fop := RingMicromega.OpLe;
                             RingMicromega.Frhs := EnvRing.PEc BinNums.Z0
                           |} tt)
                        (Tauto.A Tauto.isProp
                           {|
                             RingMicromega.Flhs :=
                               EnvRing.PEX (BinNums.xO BinNums.xH);
                             RingMicromega.Fop := RingMicromega.OpEq;
                             RingMicromega.Frhs := EnvRing.PEc BinNums.Z0
                           |} tt))) None
                  (Tauto.IMPL
                     (Tauto.A Tauto.isProp
                        {|
                          RingMicromega.Flhs :=
                            EnvRing.PEX (BinNums.xI (BinNums.xO BinNums.xH));
                          RingMicromega.Fop := RingMicromega.OpLe;
                          RingMicromega.Frhs :=
                            EnvRing.PEX (BinNums.xI BinNums.xH)
                        |} tt) None
                     (Tauto.IMPL
                        (Tauto.A Tauto.isProp
                           {|
                             RingMicromega.Flhs :=
                               EnvRing.PEX (BinNums.xI BinNums.xH);
                             RingMicromega.Fop := RingMicromega.OpLt;
                             RingMicromega.Frhs :=
                               EnvRing.PEadd
                                 (EnvRing.PEX
                                    (BinNums.xO (BinNums.xO BinNums.xH)))
                                 (EnvRing.PEX
                                    (BinNums.xI (BinNums.xO BinNums.xH)))
                           |} tt) None
                        (Tauto.A Tauto.isProp
                           {|
                             RingMicromega.Flhs := EnvRing.PEX BinNums.xH;
                             RingMicromega.Fop := RingMicromega.OpEq;
                             RingMicromega.Frhs :=
                               EnvRing.PEX (BinNums.xO BinNums.xH)
                           |} tt)))))
       : Tauto.BFormula (RingMicromega.Formula BinNums.Z) Tauto.isProp
  ============================
   (BinInt.Z.lt BinNums.Z0 (BinInt.Z.sub (BinInt.Z.add __x7 __x6) __x3)
    ∧ __x1 = BinInt.Z.sub (BinInt.Z.add __x7 __x6) __x3
    ∨ BinInt.Z.le (BinInt.Z.sub (BinInt.Z.add __x7 __x6) __x3) BinNums.Z0
      ∧ __x1 = BinNums.Z0
    → __p1 ∧ __x7 = BinInt.Z.sub __x4 (BinNums.Zpos BinNums.xH)
      ∨ BinInt.Z.le (BinInt.Z.sub __x4 (BinNums.Zpos BinNums.xH)) BinNums.Z0
        ∧ __x7 = BinNums.Z0
      → BinInt.Z.lt BinNums.Z0
          (BinInt.Z.sub (BinInt.Z.add __x4 __x6)
             (BinInt.Z.add __x3 (BinNums.Zpos BinNums.xH)))
        ∧ __x2 =
          BinInt.Z.sub (BinInt.Z.add __x4 __x6)
            (BinInt.Z.add __x3 (BinNums.Zpos BinNums.xH))
        ∨ BinInt.Z.le
            (BinInt.Z.sub (BinInt.Z.add __x4 __x6)
               (BinInt.Z.add __x3 (BinNums.Zpos BinNums.xH))) BinNums.Z0
          ∧ __x2 = BinNums.Z0
        → BinInt.Z.le __x5 __x3
          → BinInt.Z.lt __x3 (BinInt.Z.add __x4 __x5) → __x1 = __x2)


DEBUG:Going to execute:
exact
(ZMicromega.ZTautoChecker_sound __ff __wit
   (eq_refl <: ZMicromega.ZTautoChecker __ff __wit = true)
   (VarMap.find BinNums.Z0 __varmap))