Skip to main content

Browse the archive

Revision 84e3cebb5d2a7c2c7bef04ff990b5277b6b1e883 authored by Nikhil Swamy on 10 May 2017, 14:15:34 UTC, committed by Nikhil Swamy on 10 May 2017, 14:15:34 UTC 
merging master in
2 parent s 3678563 + 58c5c7e
Raw File
Spec.CTR.Lemmas.fst 
module Spec.CTR.Lemmas

open FStar.Mul

#set-options "--max_fuel 0 --initial_fuel 0"

val lemma_div: a:nat -> b:pos{a >= b} -> Lemma ((a-b)/b = a / b - 1)
let lemma_div a b =
  Math.Lemmas.lemma_div_mod a b;
  Math.Lemmas.lemma_div_mod (a-b) b;
  Math.Lemmas.lemma_mod_plus (a - b) 1 b
back to top