val lemma_inverse_one: #t:Type -> k:abelian_group t ->
  Lemma (inverse k.cm.one == k.cm.one)
let lemma_inverse_one #t k =
  lemma_inverse k.cm.one;
  assert (k.cm.mul (inverse cm.one) cm.one == cm.one);
  k.cm.lemma_one (inverse cm.one);
  assert (inverse k.cm.one == cm.one)
val lemma_inverse_one: #t:Type -> k:abelian_group t ->
  Lemma (inverse k.cm.one == k.cm.one)
let lemma_inverse_one #t k =
lemma_inverse k.cm.one;
assert (k.cm.mul (inverse cm.one) cm.one == cm.one);
k.cm.lemma_one (inverse cm.one);
assert (inverse k.cm.one == cm.one)
Lib.Exponentiation.Definition.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Lib.Exponentiation.Definition.fst
Lib.Exponentiation.Definition.abelian_group Prims._assert Prims.eq2 Lib.Exponentiation.Definition.inverse Lib.Exponentiation.Definition.__proj__Mkcomm_monoid__item__one Lib.Exponentiation.Definition.__proj__Mkabelian_group__item__cm Lib.Exponentiation.Definition.cm Prims.unit Lib.Exponentiation.Definition.__proj__Mkcomm_monoid__item__lemma_one Lib.Exponentiation.Definition.__proj__Mkcomm_monoid__item__mul Lib.Exponentiation.Definition.lemma_inverse
module Lib.Exponentiation.Definition

open FStar.Mul

module Loops = Lib.LoopCombinators

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val lemma_inverse_one: #t:Type -> k:abelian_group t ->
  Lemma (inverse k.cm.one == k.cm.one)
k: Lib.Exponentiation.Definition.abelian_group t
  -> FStar.Pervasives.Lemma
    (ensures
      Lib.Exponentiation.Definition.inverse (Mkcomm_monoid?.one (Mkabelian_group?.cm k)) ==
      Mkcomm_monoid?.one (Mkabelian_group?.cm k))