val lemma_mul_cancel_inverse: #t:Type -> k:abelian_group t -> a:t -> b:t ->
  Lemma (cm.mul (inverse a) (cm.mul a b) == b)
let lemma_mul_cancel_inverse #t k a b =
  calc (==) {
    cm.mul (inverse a) (cm.mul a b);
    (==) { cm.lemma_mul_assoc (inverse a) a b }
    cm.mul (cm.mul (inverse a) a) b;
    (==) { lemma_inverse a }
    cm.mul cm.one b;
    (==) { cm.lemma_mul_comm cm.one b }
    cm.mul b cm.one;
    (==) { cm.lemma_one b }
    b;
  }
val lemma_mul_cancel_inverse: #t:Type -> k:abelian_group t -> a:t -> b:t ->
  Lemma (cm.mul (inverse a) (cm.mul a b) == b)
let lemma_mul_cancel_inverse #t k a b =
calc ( == ) {
  cm.mul (inverse a) (cm.mul a b);
  ( == ) { cm.lemma_mul_assoc (inverse a) a b }
  cm.mul (cm.mul (inverse a) a) b;
  ( == ) { lemma_inverse a }
  cm.mul cm.one b;
  ( == ) { cm.lemma_mul_comm cm.one b }
  cm.mul b cm.one;
  ( == ) { cm.lemma_one b }
  b;
}
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 FStar.Calc.calc_finish Prims.eq2 Lib.Exponentiation.Definition.__proj__Mkcomm_monoid__item__mul Lib.Exponentiation.Definition.cm Lib.Exponentiation.Definition.inverse Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Lib.Exponentiation.Definition.__proj__Mkcomm_monoid__item__one FStar.Calc.calc_init FStar.Calc.calc_pack Lib.Exponentiation.Definition.__proj__Mkcomm_monoid__item__lemma_mul_assoc Prims.squash Lib.Exponentiation.Definition.lemma_inverse Lib.Exponentiation.Definition.__proj__Mkcomm_monoid__item__lemma_mul_comm Lib.Exponentiation.Definition.__proj__Mkcomm_monoid__item__lemma_one
module Lib.Exponentiation.Definition

open FStar.Mul

module Loops = Lib.LoopCombinators

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

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_mul_cancel_inverse: #t:Type -> k:abelian_group t -> a:t -> b:t ->
  Lemma (cm.mul (inverse a) (cm.mul a b) == b)
val lemma_mul_cancel_inverse: #t:Type -> k:abelian_group t -> a:t -> b:t ->
  Lemma (cm.mul (inverse a) (cm.mul a b) == b)
k: Lib.Exponentiation.Definition.abelian_group t -> a: t -> b: t
  -> FStar.Pervasives.Lemma
    (ensures
      Mkcomm_monoid?.mul Lib.Exponentiation.Definition.cm
        (Lib.Exponentiation.Definition.inverse a)
        (Mkcomm_monoid?.mul Lib.Exponentiation.Definition.cm a b) ==
      b)