val pow_neg (#t: Type) (k: abelian_group t) (x: t) (n: int) : t
let pow_neg (#t:Type) (k:abelian_group t) (x:t) (n:int) : t =
  if n >= 0 then pow k.cm x n else k.inverse (pow k.cm x (- n))
val pow_neg (#t: Type) (k: abelian_group t) (x: t) (n: int) : t
let pow_neg (#t: Type) (k: abelian_group t) (x: t) (n: int) : t =
if n >= 0 then pow k.cm x n else k.inverse (pow k.cm x (- n))
Lib.Exponentiation.Definition.fsti.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Lib.Exponentiation.Definition.fsti
Lib.Exponentiation.Definition.abelian_group Prims.int Prims.op_GreaterThanOrEqual Lib.Exponentiation.Definition.pow Lib.Exponentiation.Definition.__proj__Mkabelian_group__item__cm Prims.bool Lib.Exponentiation.Definition.__proj__Mkabelian_group__item__inverse Prims.op_Minus
module Lib.Exponentiation.Definition

open FStar.Mul

module Loops = Lib.LoopCombinators

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

//we don't require to have an inverse element to be an abelian group
//so this is just commutative monoid
inline_for_extraction
class comm_monoid (t:Type) = {
  one: t;
  mul: t -> t -> t;
  lemma_one: a:t -> Lemma (mul a one == a);
  lemma_mul_assoc: a:t -> b:t -> c:t -> Lemma (mul (mul a b) c == mul a (mul b c));
  lemma_mul_comm: a:t -> b:t -> Lemma (mul a b == mul b a)
  }


inline_for_extraction
class abelian_group (t:Type) = {
  cm:comm_monoid t;
  inverse: t -> t;
  lemma_inverse: a:t -> Lemma (mul (inverse a) a == one)
  }

let sqr (#t:Type) (k:comm_monoid t) (a:t) : t = mul a a


[@(strict_on_arguments [3])]
let rec pow (#t:Type) (k:comm_monoid t) (x:t) (n:nat) : t =
  if n = 0 then one
  else mul x (pow k x (n - 1))
val pow_neg (#t: Type) (k: abelian_group t) (x: t) (n: int) : t
k: Lib.Exponentiation.Definition.abelian_group t -> x: t -> n: Prims.int -> t