```
"forall(x:kk,o_kk +_kk x=x)"
lemma
(theory fields)
(proof
(
)))
```

```
"forall(x:kk, -_kk x +_kk x=o_kk)"
lemma
(theory fields)
(proof
(
)))
```

```
(def-theorem group-to-field-multiplicative-group-obl-1
"not(i_kk=o_kk)"
lemma
(theory fields)
(proof
(
(force-substitution "i_kk=o_kk" "o_kk=i_kk" (0))
(apply-macete-with-minor-premises field-zero-is-not-field-one)
simplify
)))
```

```
(def-theorem group-to-field-multiplicative-group-obl-2
"forall(x_1,x_0:kk, not(x_0=o_kk) implies x_1=o_kk or not(x_1 *_kk x_0=o_kk))"
lemma
(theory fields)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises non-o_kk-is-closed-under-*_kk)
direct-inference
)))
```

```
(def-theorem group-to-field-multiplicative-group-obl-3
"forall(x:kk, not(x=o_kk) implies if(not(i_kk=o_kk), x, ?kk)=x)"
lemma
(theory fields)
(proof
(
(raise-conditional (0))
direct-and-antecedent-inference-strategy
)))
```

```
(def-theorem group-to-field-multiplicative-group-obl-4
"forall(x:kk, not(x=o_kk) implies if(not(inv(x)=o_kk), inv(x) *_kk x, ?kk)=i_kk)"
lemma
(theory fields)
(proof
(
(apply-macete-with-minor-premises commutative-law-for-multiplication-for-fields)
(apply-macete-with-minor-premises multiplicative-inverse-for-fields)
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,not(not(p)))")
(apply-macete-with-minor-premises non-o_kk-is-closed-under-inv)
)))
```

```
(def-theorem group-to-field-multiplicative-group-obl-5
"forall(x,y,z:kk,
not(x=o_kk) and not(y=o_kk) and not(z=o_kk)
implies
if(not(y *_kk x=o_kk), z *_kk y *_kk x, ?kk)
=if(not(z *_kk y=o_kk), z *_kk y *_kk x, ?kk))"
lemma
(theory fields)
(proof
(
(raise-conditional (0))
(raise-conditional (0))
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,not(not(p)));")
(apply-macete-with-minor-premises non-o_kk-is-closed-under-*_kk)
direct-inference
(contrapose "with(p:prop,not(not(p)));")
(apply-macete-with-minor-premises non-o_kk-is-closed-under-*_kk)
direct-inference
(contrapose "with(x,y:kk,not(not(y*x=o_kk)));")
(apply-macete-with-minor-premises non-o_kk-is-closed-under-*_kk)
direct-inference
)))
```

```
(source groups)
(target fields)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(gg kk))
(constant-pairs
(e o_kk)
(mul +_kk)
(inv -_kk)))
```

```
(def-translation group-to-field-multiplicative-group
(source groups)
(target fields)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(gg (pred "lambda(z:kk,not(z=o_kk))")))
(constant-pairs
(e i_kk)
(mul "lambda(x,y:kk,if(not(x=o_kk) and not(y=o_kk), x *_kk y, ?kk))")
(inv "lambda(x:kk,if(not(x=o_kk), inv(x), ?kk))"))
(theory-interpretation-check using-simplification))
```