val pow_zero (k:pos) : Lemma (ensures pow 0 k == 0) (decreases k)
let rec pow_zero k =
  match k with
  | 1 -> ()
  | _ -> pow_zero (k - 1)
val pow_zero (k:pos) : Lemma (ensures pow 0 k == 0) (decreases k)
let rec pow_zero k =
match k with
| 1 -> ()
| _ -> pow_zero (k - 1)
FStar.Math.Fermat.fst.checked
prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Math.Euclid.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
FStar.Math.Fermat.fst
Prims.pos Prims.int FStar.Math.Fermat.pow_zero Prims.op_Subtraction Prims.unit
module FStar.Math.Fermat

open FStar.Mul
open FStar.Math.Lemmas
open FStar.Math.Euclid

#set-options "--fuel 1 --ifuel 0 --z3rlimit 20"

///
/// Pow
///

val pow_zero (k:pos) : Lemma (ensures pow 0 k == 0) (decreases k)
val pow_zero (k:pos) : Lemma (ensures pow 0 k == 0) (decreases k)
k: Prims.pos -> FStar.Pervasives.Lemma (ensures FStar.Math.Fermat.pow 0 k == 0) (decreases k)