val slash_star_axiom: a:nat -> b:pos -> c:nat -> Lemma
  (requires (a * b = c))
  (ensures  (a = c / b))
let slash_star_axiom a b c =
  lemma_div_def c b;
  lemma_mul_minus_distr_l b a (c/b)
val slash_star_axiom: a:nat -> b:pos -> c:nat -> Lemma
  (requires (a * b = c))
  (ensures  (a = c / b))
let slash_star_axiom a b c =
lemma_div_def c b;
lemma_mul_minus_distr_l b a (c / b)
FStar.Math.Lib.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
FStar.Math.Lib.fst
Prims.nat Prims.pos FStar.Math.Lib.lemma_mul_minus_distr_l Prims.op_Division Prims.unit FStar.Math.Lib.lemma_div_def
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Math.Lib

open FStar.Mul

(* Definition of the division operator *)
val lemma_div_def: a:nat -> b:pos -> Lemma (a = b * (a/b) + a % b)
let lemma_div_def a b = ()

private let mul_lemma (a:nat) (b:nat) (c:nat) : Lemma (requires (a <= b))
                                           (ensures  (c * a <= c * b))
  = ()

private let mul_lemma' (a:nat) (b:nat) (c:pos) : Lemma (requires (c * a <= c * b))
                                           (ensures (a <= b))
  = ()

private let mul_div_lemma (a:nat) (b:pos) : Lemma (b * (a / b) <= a) = ()

val slash_decr_axiom: a:nat -> b:pos -> Lemma (a / b <= a)
let slash_decr_axiom a b =
    mul_lemma 1 b a;
    mul_div_lemma a b;
    mul_lemma' (a / b) a b

private let lemma_mul_minus_distr_l (a:int) (b:int) (c:int) : Lemma (a * (b - c) = a * b - a * c)
  = ()

(* Axiom: definition of the "b divides c" relation *)
#reset-options "--z3rlimit 30"
val slash_star_axiom: a:nat -> b:pos -> c:nat -> Lemma
  (requires (a * b = c))
  (ensures  (a = c / b))
val slash_star_axiom: a:nat -> b:pos -> c:nat -> Lemma
  (requires (a * b = c))
  (ensures  (a = c / b))
a: Prims.nat -> b: Prims.pos -> c: Prims.nat
  -> FStar.Pervasives.Lemma (requires a * b = c) (ensures a = c / b)