;; 2026-06-25.  ratsqrt.scm.  Based on Forster Analysis1, constr23.pdf,
;; ss26/solheron.scm, wendler/heron.scm

#|
(load "~/git/minlog/init.scm")
(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "list.scm")
(libload "pos.scm")
(libload "int.scm")
(libload "rat.scm")
;; (set! COMMENT-FLAG #t)
|#

;; In pos.scm

;; PosExpTwoPosNatPlus
(set-goal "all p,n 2**p*2**n=2**(p+n)")
(assume "p")
(ind)
(use "Truth")
(assume "n" "IH")
(ng)
(use "IH")
;; Proof finished.
;; (cp)
(save "PosExpTwoPosNatPlus")

;; More general

;; PosExpPosNatPlus
(set-goal "all p,q,r,n (p#q)**r*(p#q)**n=(p#q)**(r+n)")
(assume "p" "q" "r")
(ind)
(ng)
(simp "PosToNatToIntId")
(use (pf "(p**r#q**r)=(p#q)**r"))
(use "Truth")
(assume "n" "IH")
(ng #t)
(simp "IH")
(use "Truth")
;; Proof finished.
;; (cp)
(save "PosExpPosNatPlus")

;; End pos.scm

;; In rat.scm

;; RatLeZeroSquare
(set-goal "all a Zero<=a*a")
(cases)
(cases)
;; 3-5
(ng)
(search)
;; 4
(ng)
(search)
;; 5
(ng)
(search)
;; Proof finished.
;; (cp)
(save "RatLeZeroSquare")

;; RatLtZeroPlus
(set-goal "all a,b(0<a -> 0<b -> 0<a+b)")
(cases)
(cases)
;; 3-5
(assume "p" "q")
(cases)
(cases)
;; 8-10
(assume "p0" "q0" "Useless1" "Useless2")
(ng)
(use "Truth")
;; 9
(ng)
(search)
;; 10
(ng)
(assume "p0" "q0" "Useless" "Absurd")
(use "EfAtom")
(use "Absurd")
;; 4
(ng)
(assume "p" "b" "Absurd" "Useless")
(use "EfAtom")
(use "Absurd")
;; 5
(ng)
(assume "p" "q" "b" "Absurd" "Useless")
(use "EfAtom")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "RatLtZeroPlus")

;; RatLtZeroTimes
(set-goal "all a,b(0<a -> 0<b -> 0<a*b)")
(cases)
(cases)
;; 3-5
(assume "p" "q")
(cases)
(cases)
;; 8-10
(assume "p0" "q0" "Useless1" "Useless2")
(ng)
(use "Truth")
;; 9
(ng)
(search)
;; 10
(ng)
(search)
;; 4
(ng)
(assume "p" "b" "Absurd" "Useless")
(use "EfAtom")
(use "Absurd")
;; 5
(ng)
(assume "p" "q" "b" "Absurd" "Useless")
(use "EfAtom")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "RatLtZeroTimes")

;; RatLtZeroUDiv
(set-goal "all a(0<a -> 0<RatUDiv a)")
(cases)
(cases)
;; 3-5
(ng)
(search)
;; 4
(ng)
(search)
;; 5
(ng)
(search)
;; Proof finished.
;; (cp)
(save "RatLtZeroUDiv")

;; RatSqPlus
(set-goal "all a,b (a+b)*(a+b)==a*a+2*a*b+b*b")
(assume "a" "b")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistrLeft")
(simprat "RatTimesPlusDistrLeft")
(simprat (pf "2*a*b==a*b+a*b"))
(ng)
(simp "RatTimesComm")
(use "Truth")
(simp "<-" "RatTimesAssoc")
(use "RatEqvSym")
(use "RatDoubleEqv")
;; Proof finished.
;; (cp)
(save "RatSqPlus")

;; RatSqMinus
(set-goal "all a,b (a+ ~b)*(a+ ~b)==a*a+ ~(2*a*b)+b*b")
(assume "a" "b")
(simprat "RatTimesPlusDistr")
(simprat "RatTimesPlusDistrLeft")
(simprat "RatTimesPlusDistrLeft")
(simprat (pf "2*a*b==a*b+a*b"))
(ng)
(simp "RatTimesComm")
(use "Truth")
(simp "<-" "RatTimesAssoc")
(use "RatEqvSym")
(use "RatDoubleEqv")
;; Proof finished.
;; (cp)
(save "RatSqMinus")

;; RatTimesUMinusId
(set-goal "all a,b ~a*b= ~(a*b)")
(assume "a")
(cases)
(cases)
(ng)
(search)
(ng)
(search)
(ng)
(search)
;; Proof finished.
;; (cp)
(save "RatTimesUMinusId")

;; RatLeZeroTimes
(set-goal "all a,b(0<=a -> 0<=b -> 0<=a*b)")
(cases)
(cases)
;; 3,4
(assume "p" "q")
(cases)
(cases)
;; 8,9
(assume "p0" "q0" "Useless1" "Useless2")
(ng)
(use "Truth")
;; 9
(ng)
(search)
;; 10
(ng)
(search)
;; 4
(ng)
(assume "p")
(cases)
(cases)
;; 18-20
(ng)
(search)
;; 19
(ng)
(search)
;; 20
(ng)
(search)
;; 5
(ng)
(assume "p" "q" "b" "Absurd" "Useless")
(use "EfAtom")
(use "Absurd")
;; Proof finished.
;; (cp)
(save "RatLeZeroTimes")

;; (set-goal "all a ~ ~a==a")
;; (assume "a")
;; (ng #t)
;; (use "Truth")
;; (save "RatUMinusUMinus")
;; Superseded by
;; (pp "RatUMinus1RewRule")
;; all a ~ ~a=a

;; RatExpConstrNatDistr
(set-goal "all p,q,n (p#q)**n=(p**n#q**n)")
(assume "p" "q")
(ind)
(use "Truth")
(assume "n" "IH")
(ng)
(simp "IH")
(use "Truth")
;; Proof finished.
;; (cp)
(save "RatExpConstrNatDistr")

(set-goal "all q,n (1#q)**n=(1#q**n)")
(assume "q")
(ind)
(use "Truth")
(assume "n" "IH")
(ng)
(simp "IH")
(use "Truth")
;; Proof finished.
(add-rewrite-rule "(1#q)**n" "(1#q**n)")

;; End of general additions to rat.scm

;; We now follow Forster to obtain approximations of sqrt(a) (for 0<a)
;; as a Cauchy sequence with modulus.  The method dates back to Heron.

;; Consider a positive rational number a, which has the form p/q.
;; We define a sequence (a_n)_n approximating sqrt(a) from above

(add-program-constant  "RatSqRtR" (py "pos=>pos=>nat=>rat"))
(add-computation-rules
 "RatSqRtR p q Zero" "p#q"
 "RatSqRtR p q(Succ n)" "([b]((1#2)*(b+(p#q)*RatUDiv b)))(RatSqRtR p q n)")

(set-totality-goal "RatSqRtR")
(fold-alltotal)
(assume "p")
(fold-alltotal)
(assume "q")
(fold-alltotal)
(ind)
;; 7,8
(use "TotalVar")
;; 8
(assume "n" "IH")
(ng)
(use "RatTimesTotal")
(use "TotalVar")
(use "RatPlusTotal")
(use "IH")
(use "RatTimesTotal")
(use "TotalVar")
(use "RatUDivTotal")
(use "IH")
;; Proof finished.
;; (cp)
(save-totality)

;; By induction an n we prove 0<a_n.

;; RatLtZeroSqRtR
(set-goal "all p,q,n 0<RatSqRtR p q n")
(assume "p" "q")
(ind)
(use "Truth")
;; Step
(assume "n" "IH")
(ng)
(use "RatLtZeroTimes")
(use "Truth")
(use "RatLtZeroPlus")
(use "IH")
(use "RatLtZeroTimes")
(use "Truth")
(use "RatLtZeroUDiv")
(use "IH")
;; Proof finished.
;; (cp)
(save "RatLtZeroSqRtR")

;; Next we aim at a<=a_{n+1}^2.  Informal proof:
;; 0<= 1/4(a_n-a/a_n)^2
;;   = 1/4(a_n^2-2a+a^2/a_n^2)
;;   = 1/4(a_n^2+2a+a^2/a_n^2)-a
;;   = a_{n+1}^2-a

;; RatSqRtRApproxLbAux
(set-goal "all b,c (1#2)*(b+c)*(1#2)*(b+c)+ ~(b*c)==(1#4)*(b+ ~c)*(b+ ~c)")
(assume "b" "c")
(use "RatEqvTrans" (pt "(1#4)*(b+c)*(b+c)+ ~(b*c)"))
;; 3,4
(use "RatTimesCompat")
(simp "<-" "RatTimesAssoc")
(simp (pf "(b+c)*(1#2)=(1#2)*(b+c)"))
(use "Truth")
(use "RatTimesComm")
(use "Truth")
;; 4
(simp "<-" "RatTimesAssoc")
(simp "<-" "RatTimesAssoc")
(simprat "RatSqPlus")
(simprat "RatSqMinus")
(use "RatEqvTrans" (pt "(1#4)*(b*b+2*b*c+c*c)+(1#4)*(4* ~(b*c))"))
;; 14,15
(use "Truth")
;; 15
(simprat "<-" "RatTimesPlusDistr")
(use "RatTimesCompat")
(use "Truth")
;; ?^18:b*b+2*b*c+c*c+4* ~(b*c)==b*b+ ~(2*b*c)+c*c
(simp "<-" "RatPlusAssoc")
(simp "<-" "RatPlusAssoc")
(simp "<-" "RatPlusAssoc")
(use "RatPlusCompat")
(use "Truth")
;; ?^23:2*b*c+(c*c+4* ~(b*c))== ~(2*b*c)+c*c
(use "RatEqvTrans" (pt "2*b*c+(4* ~(b*c)+c*c)"))
(use "RatPlusCompat")
(use "Truth")
(simp "RatPlusComm")
(use "Truth")
;; ?^25:2*b*c+(4* ~(b*c)+c*c)== ~(2*b*c)+c*c
(ng)
;; ?^29:2*b*c+ ~(4*b*c)== ~(2*b*c)
(simp "<-" "RatTimesAssoc")
(simp "<-" "RatTimesAssoc")
(simp "<-" "RatTimesUMinusId")
(simp "<-" "RatTimesUMinusId")
(simprat "<-" "RatTimesPlusDistrLeft")
(use "Truth")
;; Proof finished.
;; (cp)
(save "RatSqRtRApproxLbAux")

;; RatSqRtRApproxLb
(set-goal "all p,q,n 0<=RatSqRtR p q(Succ n)*RatSqRtR p q(Succ n)+ ~(p#q)")
(assume "p" "q" "n")
(defnc "a" "p#q")
(simp "<-" "aDef")
(defnc "b" "RatSqRtR p q n")
(defnc "c" "a*RatUDiv b")

(assert "0<b")
(simp "bDef")
(use "RatLtZeroSqRtR")
;; Assertion proved.
(assume "0<b")

(assert "0<c")
(simp "cDef")
(use "RatLtZeroTimes")
(simp "aDef")
(use "Truth")
(use "RatLtZeroUDiv")
(use "0<b")
;; Assertion proved.
(assume "0<c")

(assert "a==b*c")
(simp "cDef")
(simp "bDef")
(simp "aDef")
(ng)
(simp "<-" "aDef")
(simp "<-" "bDef")
;; ?^44:a==b*a*RatUDiv b
(simp (pf "b*a=a*b"))
(simp "<-" "RatTimesAssoc")
(simprat "RatTimesUDivR")
(use "Truth")
(simp "RatAbsId")
(use "0<b")
(use "RatLtToLe")
(use "0<b")
(use "RatTimesComm")
;; Assertion proved.
(assume "a==b*c")

;; ?^53:0<=RatSqRtR p q(Succ n)*RatSqRtR p q(Succ n)+ ~a
(ng)
;; ?^54:0<=
;;      (1#2)*(RatSqRtR p q n+(p#q)*RatUDiv(RatSqRtR p q n))*(1#2)*
;;      (RatSqRtR p q n+(p#q)*RatUDiv(RatSqRtR p q n))+ 
;;      ~a
(simp "<-" "bDef")
(simp "<-" "aDef")
(simp "<-" "cDef")
(simprat "a==b*c")
;; ?^58:0<=(1#2)*(b+c)*(1#2)*(b+c)+ ~(b*c)

;; (pp "RatSqRtRApproxLbAux")
;; all b,c (1#2)*(b+c)*(1#2)*(b+c)+ ~(b*c)==(1#4)*(b+ ~c)*(b+ ~c)

(simprat "RatSqRtRApproxLbAux")
;; ?^59:0<=(1#4)*(b+ ~c)*(b+ ~c)
(simp "<-" "RatTimesAssoc")
(use "RatLeZeroTimes")
(use "Truth")
(use "Truth")
;; Proof finished.
;; (cp)
(save "RatSqRtRApproxLb")

;; RatSqRtRApproxLbCor
(set-goal "all p,q,n (p#q)<=RatSqRtR p q(Succ n)*RatSqRtR p q(Succ n)")
(assume "p" "q" "n")
(simp (pf "(p#q)eqd~ ~(p#q)"))
;; 3,4
(use "RatZeroLePlusToUMinusLe")
(use "RatSqRtRApproxLb")
(ng)
(use "InitEqD")
;; Proof finished.
;; (cp)
(save "RatSqRtRApproxLbCor")

;; This concludes the proof of a<=a_{n+1}^2.

;; Next we prove a_{n+2}<=a_{n+1}.

;; RatSqRtRDecrSucc
(set-goal "all p,q,n RatSqRtR p q(Succ(Succ n))<=RatSqRtR p q(Succ n)")
(assume "p" "q" "n")
(defnc "a" "p#q")
(defnc "a0" "RatSqRtR p q n")
(defnc "a1" "RatSqRtR p q(Succ n)")
(defnc "a2" "RatSqRtR p q(Succ(Succ n))")
(simp "<-" "a1Def")
(simp "<-" "a2Def")
;; ?^32:a2<=a1

(assert "0<abs a1")
(simp "a1Def")
(simp "RatAbsId")
(use "RatLtZeroSqRtR")
(use "RatLtToLe")
(use "RatLtZeroSqRtR")
;; Assertion proved.
(assume "0<|a1|")

(assert "a<=a1*a1")
(simp "aDef")
(simp "a1Def")
(use "RatSqRtRApproxLbCor")
;; Assertion proved.
(assume "aBd")

(assert "a2=(1#2)*(a1+a*RatUDiv a1)")
(simp "aDef")
(simp "a1Def")
(simp "a2Def")
(ng #t)
(use "Truth")
;; Assertion proved.
(assume "a2Prop")

(simp "a2Prop")
(drop "a2Def" "a2Prop")

(use "RatLeTrans" (pt "(1#2)*(a1+a1*(a1*RatUDiv a1))"))
(use "RatLeMonTimesR")
(use "Truth")
(simprat "RatTimesUDivR")
(simp "RatTimes0RewRule")
(use "RatLeTrans" (pt "a1+a1*a1*RatUDiv a1"))
(use "RatLeMonPlus")
(use "Truth")
(use "RatLeMonTimes")
(use "RatLtToLe")
(use "RatLtZeroUDiv")
(simp "a1Def")
(use "RatLtZeroSqRtR")
(use "aBd")
;; ?^62:a1+a1*a1*RatUDiv a1<=a1+a1
(simp "<-" "RatTimesAssoc")
(simprat "RatTimesUDivR")
(simp "RatTimes0RewRule")
(use "Truth")
(use "0<|a1|")
(use "0<|a1|")
;; ?^55:(1#2)*(a1+a1*(a1*RatUDiv a1))<=a1
(simprat "RatTimesUDivR")
(simp "RatTimes0RewRule")
;; ?^76:(1#2)*(a1+a1)<=a1
(simprat "RatDoubleEqv")
(ng #t)
(use "Truth")
(use "0<|a1|")
;; Proof finished.
;; (cp)
(save "RatSqRtRDecrSucc")

;; Here the work starts.

;; 41 (1)

;; RatSqRtRDecr
(set-goal "all p,q,n,m(m<=n -> RatSqRtR p q(Succ n)<=RatSqRtR p q(Succ m))")
(assume "p" "q")
(ind)
;; 3,4
(cases)
;; 5,6
(ng)
(search)
;; 6
(ng)
(search 1 '("EfAtom" 1))
;; 4
(assume "n" "IH" "m" "m<=Sn")
(cases (pt "m=Succ n"))
(assume "m=Sn")
(simp "m=Sn")
(use "RatLeRefl")
(use "Truth")
(assume "m!=Sn")
(inst-with-to "NatLeNotEqToLt" (pt "m") (pt "Succ n") "m<=Sn" "m!=Sn" "m<Sn")
...
;; Proof finished
;; (cp)
(save "RatSqRtRDecr")

;; We define a sequence (b_n)_n approximating sqrt(a) from below

(add-program-constant "RatSqRtL" (py "pos=>pos=>nat=>rat"))
(add-computation-rules
 "RatSqRtL p q n" "(p#q)*RatUDiv(RatSqRtR p q n)")

(set-totality-goal "RatSqRtL")
(fold-alltotal)
(assume "p")
(fold-alltotal)
(assume "q")
(fold-alltotal)
(assume "n")
(ng)
(use "TotalVar")
;; Proof finished.
;; (cp)
(save-totality)

;; We prove 0<b_n.

;; 41 (2)

;; RatLtZeroSqRtL
(set-goal "all p,q,n 0<RatSqRtL p q n")
...
;; Proof finished.
;; (cp)
(save "RatLtZeroSqRtL")

;; Next we prove b_{n+1}^2<=a

;; 41 (3)

;; RatSqRtLApproxUb
(set-goal "all p,q,n RatSqRtL p q(Succ n)*RatSqRtL p q(Succ n)<=(p#q)")
(assume "p" "q" "n")
(simp "RatSqRtL0CompRule")
(defnc "a" "p#q")
(defnc "a1" "RatSqRtR p q(Succ n)")
(simp "<-" "aDef")
(simp "<-" "a1Def")
(defnc "b1" "a*RatUDiv a1")
(simp "<-" "b1Def")
;; ?^27:b1*b1<=a

(assert "RatUDiv(a1*a1)<=RatUDiv a")
(use "RatLeUDivUDiv")
(simp "aDef")
(use "Truth")
(simp "aDef")
(simp "a1Def")
(use "RatSqRtRApproxLbCor")
;; Assertion proved.
(assume "LeH")
;; ?^35:b1*b1<=a

(simp "b1Def")
(use "RatLeTrans" (pt "a*a*(RatUDiv a1*RatUDiv a1)"))
...
;; Proof finished.
;; (cp)
(save "RatSqRtLApproxUb")

;; Next we prove b_{n+1}<=b_{n+2}

;; 42 (4)

;; RatSqRtLIncrSucc
(set-goal "all p,q,n RatSqRtL p q(Succ n)<=RatSqRtL p q(Succ(Succ n))")
(assume "p" "q" "n")
(simp "RatSqRtL0CompRule")
...
;; Proof finished.
;; (cp)
(save "RatSqRtLIncrSucc")

;; 42 (5)

;; RatSqRtLIncr
(set-goal "all p,q,n,m(m<=n -> RatSqRtL p q(Succ m)<=RatSqRtL p q(Succ n))")
(assume "p" "q")
(ind)
(cases)
;; 5,6
(ng)
(search)
;; 6
(ng)
(search 1 '("EfAtom" 1))
;; 4
(assume "n" "IH" "m" "m<=Sn")
(cases (pt "m=Succ n"))
(assume "m=Sn")
...
(assume "m!=Sn")
(inst-with-to "NatLeNotEqToLt" (pt "m") (pt "Succ n") "m<=Sn" "m!=Sn" "m<Sn")
...
(use "RatSqRtLIncrSucc")
;; Proof finished
;; (cp)
(save "RatSqRtLIncr")

;; Next we aim at b_{n+1}<=a_{m+1}.  Informal proof:
;; Let m<=n.  Then
;; b_{n+1} =a/a_{n+1}
;;        <=a_{n+1} from a<=a_{n+1}^2 by multiplying with 1/a_{n+1}
;;        <=a_{m+1} by RatSqRtRDecr

;; 42 (6)
;; RatSqRtLeLR
(set-goal "all p,q,n RatSqRtL p q(Succ n)<=RatSqRtR p q(Succ n)")
(assume "p" "q" "n")
(simp "RatSqRtL0CompRule")
(use "RatLeTrans" (pt "RatSqRtR p q(Succ n)*RatSqRtR p q(Succ n)*
                       RatUDiv(RatSqRtR p q(Succ n))"))
(use "RatLeMonTimes")
(use "RatLtToLe")
(use "RatLtZeroUDiv")
(use "RatLtZeroSqRtR")
;; ?^7:(p#q)<=RatSqRtR p q(Succ n)*RatSqRtR p q(Succ n)
(simp "<-" "RatUMinus1RewRule")
;; ?^10:~ ~(p#q)<=RatSqRtR p q(Succ n)*RatSqRtR p q(Succ n)
(use "RatZeroLePlusToUMinusLe")
...
;; Proof finished
;; (cp)
(save "RatSqRtLeLR")

;; 43 (7)

;; Useful theorems:
(pp "RatUMinusLeToZeroLePlus")
;; all a,b(~b<=a -> 0<=a+b)
(pp "RatUMinus1RewRule")
;; all a ~ ~a=a

;; RatSqRtRLDiff
(set-goal "all p,q,n 
     RatSqRtR p q(Succ n)+ ~(RatSqRtL p q(Succ n))<=
     (1#2**n)*(RatSqRtR p q(PosToNat 1)+ ~(RatSqRtL p q(PosToNat 1)))")
(assume "p" "q")
(ind)
(ng #t)
(use "Truth")
(assume "n" "IH")
(assert "RatSqRtR p q(Succ(Succ n))==
         (1#2)*(RatSqRtR p q(Succ n)+RatSqRtL p q(Succ n))")
(use "Truth")
(assume "Eq")
(simprat "Eq")
(use "RatLeTrans" (pt "(1#2)*(RatSqRtR p q(Succ n)+RatSqRtL p q(Succ n))+
     ~(RatSqRtL p q(Succ n))"))
(use "RatLeMonPlus")
(use "RatLeRefl")
(use "Truth")
(simp "RatLeUMinus")
(use "RatSqRtLIncrSucc")
(use "RatLeTrans" (pt "(1#2)*(RatSqRtR p q(Succ n)+ ~(RatSqRtL p q(Succ n)))"))
(use "RatLeRefl")
(simprat "RatTimesPlusDistr")
(assert "~(RatSqRtL p q(Succ n))== ~(1#2)*2*(RatSqRtL p q(Succ n))")
(ng #t)
(use "Truth")
(assume "Eq2")
(simprat "Eq2")
(simp "<-" "RatPlusAssoc")
(simprat "<-" "RatTimesPlusDistrLeft")
(assert "((1#2)+ ~(1#2)*2)*RatSqRtL p q(Succ n)==
          (1#2)*(~(RatSqRtL p q(Succ n)))")
(ng #t)
(use "Truth")
(assume "Eq3")
(simprat "Eq3")
(simprat "<-" "Eq2")
(simprat "<-" "RatTimesPlusDistr")
(use "Truth")

;; ?^18:(1#2)*(RatSqRtR p q(Succ n)+ ~(RatSqRtL p q(Succ n)))<=
;;      (1#2**Succ n)*(RatSqRtR p q(PosToNat 1)+ ~(RatSqRtL p q(PosToNat 1)))
(assert "(1#2**Succ n)=(1#2)*(1#2)**n")
(ng #t)
(use "Truth")
(assume "Eq4")
(simp "Eq4")
...
;; Proof finished
;; (cp)
(save "RatSqRtRLDiff")

;; We construct a modulus for (a_{n+1})_n.  More precisely, fix p,q,l
;; such that RatSqRtR p q(Succ Zero)+ ~(RatSqRtL p q(Succ Zero))<=2**l.
;; We show that M(r) := r+l is a modulus for the Cauchy sequence
;; (a_{n+1})_n.

;; 43 (8)

;; Useful theorem:
(pp "PosExpTwoPosNatPlus")
;; all p,n 2**p*2**n=2**(p+n)

;; RatSqRtRModul
(set-goal "all p,q,l(
     RatSqRtR p q(Succ Zero)+ ~(RatSqRtL p q(Succ Zero))<=2**l -> 
     all r,n,m(
      r+l<=m -> 
      m<=n -> RatSqRtR p q(Succ m)+ ~(RatSqRtR p q(Succ n))<=(1#2**r)))")
(assume "p" "q" "l" "LeH" "r" "n" "m" "r+l<=m" "m<=n")

(assert "2**(r+l)<=2**m")
(use "NatLeMonTwoExp")
(use "r+l<=m")
;; Assertion proved.
(assume "A1")
;; ?^6:RatSqRtR p q(Succ m)+ ~(RatSqRtR p q(Succ n))<=(1#2**r)
(use "RatLeTrans" (pt "RatSqRtR p q(Succ m)+ ~(RatSqRtL p q(Succ m))"))
;; 7,8
...
;; 8
(use "RatLeTrans"
     (pt "(1#2**m)*(RatSqRtR p q(Succ Zero)+ ~(RatSqRtL p q(Succ Zero)))"))
;; 15,16
;; ?^15:RatSqRtR p q(Succ m)+ ~(RatSqRtL p q(Succ m))<=
;;      (1#2**m)*(RatSqRtR p q(Succ Zero)+ ~(RatSqRtL p q(Succ Zero)))
;; (pp "RatSqRtRLDiff")
(simp (pf "Succ Zero=PosToNat 1"))
(use "RatSqRtRLDiff")
(use "Truth")
;; ?^16:(1#2**m)*(RatSqRtR p q(Succ Zero)+ ~(RatSqRtL p q(Succ Zero)))<=(1#2**r)
...
;; Proof finished.
;; (cp)
(save "RatSqRtRModul")