Add KD proof for 11^n-4^n divides 7

Documentation/SBV/Examples/KnuckleDragger/Induction.hs

@@ -80,3 +80,26 @@ sumSquareProof = runKD $ do
        p n = observe "imp" (sumSquare n) .== observe "spec" (spec n)
 
    lemma "sumSquare_correct" (\(Forall @"n" n) -> n .>= 0 .=> p n) [induct p]
+
+-- | Prove that @11^n - 4^n@ is always divisible by 7. Note that power operator is hard for
+-- SMT solvers to deal with due to non-linearity, so we use an axiomatization of it instead.
+--
+-- We have:
+--
+-- >>> elevenMinusFour
+-- Axiom: pow0                             Axiom.
+-- Axiom: powN                             Axiom.
+-- Lemma: elevenMinusFour                  Q.E.D.
+-- [Proven] elevenMinusFour
+elevenMinusFour :: IO Proof
+elevenMinusFour = runKD $ do
+   let pow :: SInteger -> SInteger -> SInteger
+       pow = uninterpret "pow"
+
+       emf :: SInteger -> SBool
+       emf n = 7 `sDivides` (11 `pow` n - 4 `pow` n)
+
+   pow0 <- axiom "pow0" (\(Forall @"x" x)                 -> x `pow` 0     .== 1)
+   powN <- axiom "powN" (\(Forall @"x" x) (Forall @"n" n) -> x `pow` (n+1) .== x * x `pow` n)
+
+   lemma "elevenMinusFour" (\(Forall @"n" n) -> n .>= 0 .=> emf n) [pow0, powN, induct emf]