Goal:
  
  __p1 : Prop
  __x7 : BinNums.Z
  __x6 : BinNums.Z
  __x5 : BinNums.Z
  __x4 : BinNums.Z
  __x3 : BinNums.Z
  __x2 : BinNums.Z
  __x1 : BinNums.Z
  ============================
   (let __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]
      in
    let __varmap :=
      VarMap.Branch (VarMap.Branch (VarMap.Elt __x4) __x2 (VarMap.Elt __x6))
        __x1 (VarMap.Branch (VarMap.Elt __x5) __x3 (VarMap.Elt __x7)) in
    let __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))))) in
    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:
let __wit := fresh "__wit" in
           let __varmap := fresh "__varmap" in
           let __ff := fresh "__ff" in
           intros __wit __varmap __ff; exact
            (ZMicromega.ZTautoChecker_sound __ff __wit
               (eq_refl <: ZMicromega.ZTautoChecker __ff __wit = true)
               (VarMap.find BinNums.Z0 __varmap))