```
(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)
)
```

```
(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)
```(def-overloading delta