(def-theorem group-to-field-additive-group-obl-1 
    "forall(x:kk,o_kk +_kk x=x)"
    lemma
    (theory fields)
    (proof
      (
        (apply-macete-with-minor-premises commutative-law-for-addition-for-fields)
        (apply-macete-with-minor-premises additive-identity-for-fields)
        )))

(def-theorem group-to-field-additive-group-obl-2 
    "forall(x:kk, -_kk x +_kk x=o_kk)"
    lemma
    (theory fields)
    (proof
      (
        (apply-macete-with-minor-premises commutative-law-for-addition-for-fields)
        (apply-macete-with-minor-premises additive-inverse-for-fields)
        )))

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

(def-translation group-to-field-additive-group 
    (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))