(def-translation monoids-to-groups 
    (source monoid-theory)
    (target groups)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs (uu gg))
    (constant-pairs
      (e e)
      (** mul)))

(def-constant minus 
    "lambda(x,y:gg,inv(y) mul x)"
    (theory groups)
    (usages rewrite))

(def-transported-symbols (monoid%prod)
    (translation monoids-to-groups)
    (renamer monoid-to-groups-renamer)
    )

(def-translation groups-to-additive-rr 
    (source groups)
    (target h-o-real-arithmetic)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs
      (gg rr))
    (constant-pairs
      (e 0)
      (mul  +)
      (inv -)
      (minus sub)
      (group%prod sum))
    (theory-interpretation-check using-simplification))

(def-constant delta 
    "lambda(f:[zz,gg],lambda(n:zz,minus(f(n+1),f(n))))"
    (theory groups)
    (usages rewrite))

(def-theorem telescoping-prod-formula 
    "forall(f:[zz,gg],m,n:zz,m<=n and
                                forall(j:zz,(m<=j and j<=n+1) implies #(f(j)))
                                      implies group%prod(m,n,delta(f))=minus(f(n+1),f(m)))"
    (theory  groups)
    (usages transportable-macete)
    (proof
      (
        (induction integer-inductor ())
        (prove-by-logic-and-simplification 3)
        (backchain "with(f:[zz,gg],t,m:zz,
    forall(j:zz,m<=j and j<=1+t implies #(f(j)))
      implies 
    group%prod(m,t,lambda(n:zz,inv(f(n)) mul f(1+n)))
    =inv(f(m)) mul f(1+t));")
        direct-and-antecedent-inference-strategy
        simplify
        simplify
        )))

(def-transported-symbols (delta)
    (translation groups-to-additive-rr)
    (renamer groups-to-additive-rr-renamer)
    )

(def-overloading delta
    (groups delta) (h-o-real-arithmetic rr%delta))