fsdoc: no-summary-found
fsdoc: no-comment-found
val modulo_lemma:Unidentified product: [a:nat] Unidentified product: [b:pos] (Lemma ((requires (<(a, b)))) ((ensures (=(%(a, b), a)))))Same as small_mod
val lemma_div_mod:Unidentified product: [a:int] Unidentified product: [p:nonzero] (Lemma (=(a, +(*(p, (/(a, p))), %(a, p)))))Same as lemma_div_def in Math.Lib