val lemma_inverse_mul: #t:Type -> k:abelian_group t -> a:t -> b:t ->
  Lemma (inverse (cm.mul a b) == cm.mul (inverse a) (inverse b))
let lemma_inverse_mul #t k a b =
  lemma_inverse (cm.mul a b);
  cm.lemma_mul_comm (inverse (cm.mul a b)) (cm.mul a b);
  assert (cm.mul (cm.mul a b) (inverse (cm.mul a b)) == cm.one);
  calc (==) {
    cm.mul (cm.mul a b) (cm.mul (inverse a) (inverse b));
    (==) { cm.lemma_mul_assoc (cm.mul a b) (inverse a) (inverse b) }
    cm.mul (cm.mul (cm.mul a b) (inverse a)) (inverse b);
    (==) { cm.lemma_mul_comm (cm.mul a b) (inverse a) }
    cm.mul (cm.mul (inverse a) (cm.mul a b)) (inverse b);
    (==) { lemma_mul_cancel_inverse k a b }
    cm.mul b (inverse b);
    (==) { cm.lemma_mul_comm b (inverse b) }
    cm.mul (inverse b) b;
    (==) { lemma_inverse b }
    cm.one;
  };

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

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_cancellation: #t:Type -> k:abelian_group t -> a:t -> b:t -> c:t -> Lemma
  (requires cm.mul a b == cm.mul a c)
  (ensures  b == c)

let lemma_cancellation #t k a b c =
  assert (cm.mul (inverse a) (cm.mul a b) == cm.mul (inverse a) (cm.mul a c));
  lemma_mul_cancel_inverse #t k a b;
  lemma_mul_cancel_inverse #t k a c


let lemma_inverse_id #t k a =
  lemma_inverse a;
  lemma_inverse (inverse a);
  assert (cm.mul (inverse a) a == cm.one);
  assert (cm.mul (inverse (inverse a)) (inverse a) == cm.one);
  cm.lemma_mul_comm (inverse (inverse a)) (inverse a);
  lemma_cancellation k (inverse a) a (inverse (inverse a));
  assert (a == (inverse (inverse a)))
val lemma_inverse_mul: #t:Type -> k:abelian_group t -> a:t -> b:t ->
  Lemma (inverse (cm.mul a b) == cm.mul (inverse a) (inverse b))
k: Lib.Exponentiation.Definition.abelian_group t -> a: t -> b: t
  -> FStar.Pervasives.Lemma
    (ensures
      Lib.Exponentiation.Definition.inverse (Mkcomm_monoid?.mul Lib.Exponentiation.Definition.cm a b
        ) ==
      Mkcomm_monoid?.mul Lib.Exponentiation.Definition.cm
        (Lib.Exponentiation.Definition.inverse a)
        (Lib.Exponentiation.Definition.inverse b))