content: -----------------------------------------------------------------------------
  -- |
  -- Module    : Documentation.SBV.Examples.TP.PowerMod
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Proofs about power and modulus. Adapted from an example by amigalemming,
  -- see <http://github.com/LeventErkok/sbv/issues/744>.
  --
  -- We also demonstrate the proof-caching features of TP.
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE TypeAbstractions    #-}
  {-# LANGUAGE TypeApplications    #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module Documentation.SBV.Examples.TP.PowerMod where
  
  import Data.SBV
  import Data.SBV.TP
  
  -- | The proofs in this module are structured so they are presented at the top-level and reused.
  -- This results in re-running the proofs over and over, as each proof has to run all its dependents.
  -- To avoid re-running proofs, we tell TP to use a proof-cache. Note that use of a proof-cache comes
  -- with the user obligation that all proofs used are uniquely named. Otherwise the results can be
  -- unsound, and SBV will indicate this possibility in its output.
  runCached :: TP a -> IO a
  runCached = runTPWith (tpCache z3)
  
  -- | Power function over integers.
  power :: SInteger -> SInteger -> SInteger
  power = smtFunction "power" $ \b n -> ite (n .<= 0) 1 (b * power b (n-1))
  
  -- | \(m > 1 \Rightarrow n + mk \equiv n \pmod{m}\)
  --
  -- ==== __Proof__
  -- >>> runCached modAddMultiple
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] modAddMultiple :: Ɐk ∷ Integer → Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
  modAddMultiple :: TP (Proof (Forall "k" Integer -> Forall "n" Integer -> Forall "m" Integer -> SBool))
  modAddMultiple = do
     inductWith (tpCache cvc5) "modAddMultiple"
        (\(Forall k) (Forall n) (Forall m) -> m .> 1 .=> (n + m*k) `sEMod` m .== n `sEMod` m) $
        \ih k n m -> [m .> 1] |- (n + m*(k+1)) `sEMod` m
                                =: (n + m*k + m) `sEMod` m
                                =: (n + m*k) `sEMod` m
                                ?? ih `at` (Inst @"n" n, Inst @"m" m)
                                =: n `sEMod` m
                                =: qed
  
  -- | \(m > 0 \Rightarrow a + b \equiv a + (b \bmod m) \pmod{m}\)
  --
  -- ==== __Proof__
  -- >>> runCached modAddRight
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] modAddRight :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
  modAddRight :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
  modAddRight = do
     mAddMul <- modAddMultiple
     calc "modAddRight"
        (\(Forall a) (Forall b) (Forall m) -> m .> 0  .=>  (a+b) `sEMod` m .== (a + b `sEMod` m) `sEMod` m) $
        \a b m -> [m .> 0] |- (a+b) `sEMod` m
                           =: (a + b `sEMod` m + m * b `sEDiv` m) `sEMod` m
                           ?? mAddMul `at` (Inst @"k" (b `sEDiv` m), Inst @"n" (a + b `sEMod` m), Inst @"m" m)
                           =: (a + b `sEMod` m) `sEMod` m
                           =: qed
  
  -- | \(m > 0 \Rightarrow a + b \equiv (a \bmod m) + b \pmod{m}\)
  --
  -- ==== __Proof__
  -- >>> runCached modAddLeft
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] modAddLeft :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
  modAddLeft :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
  modAddLeft = do
     mAddR <- modAddRight
     calc "modAddLeft"
        (\(Forall a) (Forall b) (Forall m) -> m .> 0 .=>  (a+b) `sEMod` m .== (a `sEMod` m + b) `sEMod` m) $
        \a b m -> [m .> 0] |- (a+b) `sEMod` m
                           =: (b+a) `sEMod` m
                           ?? mAddR
                           =: (b + a `sEMod` m) `sEMod` m
                           =: (a `sEMod` m + b) `sEMod` m
                           =: qed
  
  -- | \(m > 0 \Rightarrow a - b \equiv a - (b \bmod m) \pmod{m}\)
  --
  -- ==== __Proof__
  -- >>> runCached modSubRight
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modSubRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] modSubRight :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
  modSubRight :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
  modSubRight = do
     mAddMul <- modAddMultiple
     calc "modSubRight"
        (\(Forall a) (Forall b) (Forall m) -> m .> 0 .=>  (a-b) `sEMod` m .== (a - b `sEMod` m) `sEMod` m) $
        \a b m -> [m .> 0] |- (a - b) `sEMod` m
                           ?? b .== b `sEMod` m + m * b `sEDiv` m
                           =: (a - (b `sEMod` m + m * b `sEDiv` m)) `sEMod` m
                           =: ((a - b `sEMod` m) + m * (- (b `sEDiv` m))) `sEMod` m
                           ?? mAddMul `at` (Inst @"k" (- (b `sEDiv` m)), Inst @"n" (a - b `sEMod` m), Inst @"m" m)
                           =: (a - b `sEMod` m) `sEMod` m
                           =: qed
  
  -- | \(a \geq 0 \land m > 0 \Rightarrow ab \equiv a \cdot (b \bmod m) \pmod{m}\)
  --
  -- ==== __Proof__
  -- >>> runCached modMulRightNonneg
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Inductive lemma: modMulRightNonneg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven. Cached: modAddRight] modMulRightNonneg :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
  modMulRightNonneg :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
  modMulRightNonneg = do
     mAddL <- modAddLeft
     mAddR <- modAddRight
  
     induct "modMulRightNonneg"
        (\(Forall a) (Forall b) (Forall m) -> a .>= 0 .&& m .> 0 .=> (a*b) `sEMod` m .== (a * b `sEMod` m) `sEMod` m) $
        \ih a b m -> [a .>= 0, m .> 0] |- ((a+1)*b) `sEMod` m
                                       =: (a*b+b) `sEMod` m
                                       ?? mAddR `at` (Inst @"a" (a*b), Inst @"b" b, Inst @"m" m)
                                       =: (a*b + b `sEMod` m) `sEMod` m
                                       ?? mAddL `at` (Inst @"a" (a*b), Inst @"b" (b `sEMod` m), Inst @"m" m)
                                       =: ((a*b) `sEMod` m + b `sEMod` m) `sEMod` m
                                       ?? ih `at` (Inst @"b" b, Inst @"m" m)
                                       =: ((a * b `sEMod` m) `sEMod` m + b `sEMod` m) `sEMod` m
                                       ?? mAddL
                                       =: (a * b `sEMod` m + b `sEMod` m) `sEMod` m
                                       =: ((a+1) * b `sEMod` m) `sEMod` m
                                       =: qed
  
  -- | \(a \geq 0 \land m > 0 \Rightarrow -ab \equiv -\left(a \cdot (b \bmod m)\right) \pmod{m}\)
  --
  -- ==== __Proof__
  -- >>> runCached modMulRightNeg
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Lemma: modSubRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: modMulRightNeg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven. Cached: modAddMultiple] modMulRightNeg :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
  modMulRightNeg :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
  modMulRightNeg = do
     mAddL <- modAddLeft
     mSubR <- modSubRight
  
     induct "modMulRightNeg"
        (\(Forall a) (Forall b) (Forall m) -> a .>= 0 .&& m .> 0 .=> (-(a*b)) `sEMod` m .== (-(a * b `sEMod` m)) `sEMod` m) $
        \ih a b m -> [a .>= 0, m .> 0] |- (-((a+1)*b)) `sEMod` m
                                       =: (-(a*b)-b) `sEMod` m
                                       ?? mSubR `at` (Inst @"a" (-(a*b)), Inst @"b" b, Inst @"m" m)
                                       =: (-(a*b) - b `sEMod` m) `sEMod` m
                                       ?? mAddL `at` (Inst @"a" (-(a*b)), Inst @"b" (- (b `sEMod` m)), Inst @"m" m)
                                       =: ((-(a*b)) `sEMod` m - b `sEMod` m) `sEMod` m
                                       ?? ih `at` (Inst @"b" b, Inst @"m" m)
                                       =: ((-(a * b `sEMod` m)) `sEMod` m - b `sEMod` m) `sEMod` m
                                       ?? mAddL
                                       =: (-(a * b `sEMod` m) - b `sEMod` m) `sEMod` m
                                       =: (-((a+1) * b `sEMod` m)) `sEMod` m
                                       =: qed
  
  -- | \(m > 0 \Rightarrow ab \equiv a \cdot (b \bmod m) \pmod{m}\)
  --
  -- ==== __Proof__
  -- >>> runCached modMulRight
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Inductive lemma: modMulRightNonneg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Lemma: modSubRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: modMulRightNeg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modMulRight
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.2.3                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven. Cached: modAddLeft, modAddMultiple, modAddRight] modMulRight :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
  modMulRight :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
  modMulRight = do
     mMulNonneg <- modMulRightNonneg
     mMulNeg    <- modMulRightNeg
  
     calc "modMulRight"
          (\(Forall a) (Forall b) (Forall m) -> m .> 0 .=> (a*b) `sEMod` m .== (a * b `sEMod` m) `sEMod` m) $
          \a b m -> [m .> 0] |- cases [ a .>= 0 ==> (a*b) `sEMod` m
                                                 ?? mMulNonneg `at` (Inst @"a" a, Inst @"b" b, Inst @"m" m)
                                                 =: (a * b `sEMod` m) `sEMod` m
                                                 =: qed
                                      , a .<  0 ==> (a*b) `sEMod` m
                                                 =: (-((-a)*b)) `sEMod` m
                                                 ?? mMulNeg `at` (Inst @"a" (-a), Inst @"b" b, Inst @"m" m)
                                                 =: (-((-a) * b `sEMod` m)) `sEMod` m
                                                 =: (a * b `sEMod` m) `sEMod` m
                                                 =: qed
                                      ]
  
  -- | \(m > 0 \Rightarrow ab \equiv (a \bmod m) \cdot b \pmod{m}\)
  --
  -- ==== __Proof__
  -- >>> runCached modMulLeft
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Inductive lemma: modMulRightNonneg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Lemma: modSubRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: modMulRightNeg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modMulRight
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.2.3                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modMulLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven. Cached: modAddLeft, modAddMultiple, modAddRight] modMulLeft :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
  modMulLeft :: TP (Proof (Forall "a" Integer -> Forall "b" Integer -> Forall "m" Integer -> SBool))
  modMulLeft = do
     mMulR <- modMulRight
  
     calc "modMulLeft"
          (\(Forall a) (Forall b) (Forall m) -> m .> 0 .=> (a*b) `sEMod` m .== (a `sEMod` m * b) `sEMod` m) $
          \a b m -> [m .> 0] |- (a*b) `sEMod` m
                             =: (b*a) `sEMod` m
                             ?? mMulR
                             =: (b * a `sEMod` m) `sEMod` m
                             =: (a `sEMod` m * b) `sEMod` m
                             =: qed
  
  -- | \(n \geq 0 \land m > 0 \Rightarrow b^n \equiv (b \bmod m)^n \pmod{m}\)
  --
  -- ==== __Proof__
  -- >>> runCached powerMod
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Inductive lemma: modMulRightNonneg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Lemma: modSubRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: modMulRightNeg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modMulRight
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.2.3                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modMulLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modMulRightNonneg               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modSubRight                     Q.E.D.
  -- Cached: modMulRightNeg                  Q.E.D.
  -- Cached: modMulRight                     Q.E.D.
  -- Inductive lemma: powerModInduct
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: powerMod                         Q.E.D.
  -- [Proven. Cached: modAddLeft, modAddMultiple, modAddRight, modMulRight] powerMod :: Ɐb ∷ Integer → Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
  powerMod :: TP (Proof (Forall "b" Integer -> Forall "n" Integer -> Forall "m" Integer -> SBool))
  powerMod = do
     mMulL <- modMulLeft
     mMulR <- modMulRight
  
     -- We want to write the b parameter first, but need to induct on n. So, this helper rearranges the parameters only.
     pMod <- induct "powerModInduct"
        (\(Forall @"n" n) (Forall @"m" m) (Forall @"b" b) -> n .>= 0 .&& m .> 0 .=> power b n `sEMod` m .== power (b `sEMod` m) n `sEMod` m) $
        \ih n m b -> [n .>= 0, m .> 0] |- power b (n+1) `sEMod` m
                                       =: (power b n * b) `sEMod` m
                                       ?? mMulL `at` (Inst @"a" (power b n), Inst @"b" b, Inst @"m" m)
                                       =: (power b n `sEMod` m * b) `sEMod` m
                                       ?? ih `at` (Inst @"m" m, Inst @"b" b)
                                       =: (power (b `sEMod` m) n `sEMod` m * b) `sEMod` m
                                       ?? mMulL `at` (Inst @"a" (power (b `sEMod` m) n), Inst @"b" b, Inst @"m" m)
                                       =: (power (b `sEMod` m) n * b) `sEMod` m
                                       ?? mMulR `at` (Inst @"a" (power (b `sEMod` m) n), Inst @"b" b, Inst @"m" m)
                                       =: (power (b `sEMod` m) n * b `sEMod` m) `sEMod` m
                                       =: power (b `sEMod` m) (n+1) `sEMod` m
                                       =: qed
  
     -- Same as above, just a more natural selection of variable order.
     lemma "powerMod"
           (\(Forall b) (Forall n) (Forall m) -> n .>= 0 .&& m .> 0 .=> power b n `sEMod` m .== power (b `sEMod` m) n `sEMod` m)
           [proofOf pMod]
  
  -- | \(n \geq 0 \Rightarrow 1^n = 1\)
  --
  -- ==== __Proof__
  -- >>> runCached onePower
  -- Inductive lemma: onePower
  --   Step: Base                            Q.E.D.
  --   Step: 1 (unfold power)                Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven] onePower :: Ɐn ∷ Integer → Bool
  onePower :: TP (Proof (Forall "n" Integer -> SBool))
  onePower = induct "onePower"
                    (\(Forall n) -> n .>= 0 .=> power 1 n .== 1) $
                    \ih n -> [] |- power 1 (n+1)
                                 ?? "unfold power"
                                 =: 1 * power 1 n
                                 ?? ih
                                 =: (1 :: SInteger)
                                 =: qed
  
  -- | \(n \geq 0 \Rightarrow (27^n \bmod 13) = 1\)
  --
  -- ==== __Proof__
  -- >>> runCached powerOf27
  -- Inductive lemma: onePower
  --   Step: Base                            Q.E.D.
  --   Step: 1 (unfold power)                Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Inductive lemma: modMulRightNonneg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Lemma: modSubRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: modMulRightNeg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modMulRight
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.2.3                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modMulLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modMulRightNonneg               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modSubRight                     Q.E.D.
  -- Cached: modMulRightNeg                  Q.E.D.
  -- Cached: modMulRight                     Q.E.D.
  -- Inductive lemma: powerModInduct
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: powerMod                         Q.E.D.
  -- Lemma: powerOf27
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven. Cached: modAddLeft, modAddMultiple, modAddRight, modMulRight] powerOf27 :: Ɐn ∷ Integer → Bool
  powerOf27 :: TP (Proof (Forall "n" Integer -> SBool))
  powerOf27 = do
     pOne <- onePower
     pMod <- powerMod
     calc "powerOf27" (\(Forall n) -> n .>= 0 .=> power 27 n `sEMod` 13 .== 1) $
                      \n -> [n .>= 0]
                         |- power 27 n `sEMod` 13
                         ?? pMod `at` (Inst @"b" 27, Inst @"n" n, Inst @"m" 13)
                         =: power (27 `sEMod` 13) n `sEMod` 13
                         =: power 1 n `sEMod` 13
                         ?? pOne
                         =: 1 `sEMod` 13
                         =: (1 :: SInteger)
                         =: qed
  
  -- | \(n \geq 0 \wedge m > 0 \implies (27^{\frac{n}{3}} \bmod 13) \cdot 3^{n \bmod 3} \equiv 3^{n \bmod 3} \pmod{m}\)
  --
  -- ==== __Proof__
  -- >>> runCached powerOfThreeMod13VarDivisor
  -- Inductive lemma: onePower
  --   Step: Base                            Q.E.D.
  --   Step: 1 (unfold power)                Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: modAddMultiple
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modAddLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Inductive lemma: modMulRightNonneg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Lemma: modSubRight
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Inductive lemma: modMulRightNeg
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modMulRight
  --   Step: 1 (2 way case split)
  --     Step: 1.1                           Q.E.D.
  --     Step: 1.2.1                         Q.E.D.
  --     Step: 1.2.2                         Q.E.D.
  --     Step: 1.2.3                         Q.E.D.
  --     Step: 1.Completeness                Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: modMulLeft
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modMulRightNonneg               Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modAddRight                     Q.E.D.
  -- Cached: modAddLeft                      Q.E.D.
  -- Cached: modAddMultiple                  Q.E.D.
  -- Cached: modSubRight                     Q.E.D.
  -- Cached: modMulRightNeg                  Q.E.D.
  -- Cached: modMulRight                     Q.E.D.
  -- Inductive lemma: powerModInduct
  --   Step: Base                            Q.E.D.
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Step: 5                               Q.E.D.
  --   Step: 6                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: powerMod                         Q.E.D.
  -- Lemma: powerOf27
  --   Step: 1                               Q.E.D.
  --   Step: 2                               Q.E.D.
  --   Step: 3                               Q.E.D.
  --   Step: 4                               Q.E.D.
  --   Result:                               Q.E.D.
  -- Lemma: powerOfThreeMod13VarDivisor
  --   Step: 1                               Q.E.D.
  --   Result:                               Q.E.D.
  -- [Proven. Cached: modAddLeft, modAddMultiple, modAddRight, modMulRight] powerOfThreeMod13VarDivisor :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
  powerOfThreeMod13VarDivisor :: TP (Proof (Forall "n" Integer -> Forall "m" Integer -> SBool))
  powerOfThreeMod13VarDivisor = do
     p27 <- powerOf27
     calc "powerOfThreeMod13VarDivisor"
          (\(Forall n) (Forall m) ->
              n .>= 0 .&& m .> 0 .=>     power 27 (n `sEDiv` 3) `sEMod` 13 * power 3 (n `sEMod` 3) `sEMod` m
                                     .== power  3 (n `sEMod` 3) `sEMod` m) $
          \n m -> [n .>= 0, m .> 0]
               |- power 27 (n `sEDiv` 3) `sEMod` 13 * power 3 (n `sEMod` 3) `sEMod` m
               ?? p27 `at` Inst @"n" (sEDiv n 3)
               =: power 3 (n `sEMod` 3) `sEMod` m
               =: qed
  