1/-1 %// 2 cases not validating or computing

[briangmilnes]

Folks,
Working out a binary search and it's convenient to run the upper bound to -1. But alas, the SMT and compute() both
don't seem to like 1/-1 %// 2. Is there an SMT axiom missing? Why doesn't compute normalizing by prims get this?

open FStar.Math
open FStar.Tactics

let lemma_zero_div_two (i: int{i = 0}) : Lemma (i / 2 = 0) = ()
let lemma_zero_mod_two (i: int{i = 0}) : Lemma (i % 2 = 0) = ()

let lemma_one_div_two (i: int{i = 1}) : Lemma (i / 2 = 0) = ()
let lemma_minus_two_div_two (i: int{i = -2}) : Lemma (i / 2 = -1) = ()

[@@ expect_failure]
let lemma_minus_one_div_two (i: int{i = -1}) : Lemma (i / 2 = 0) = assert(i / 2 = 0) by compute()

[@@ expect_failure]
let lemma_one_mod_two (i: int{i = 1}) : Lemma (i % 2 = 0) = ()
[@@ expect_failure]
let lemma_one_mod_two' (i: int{i = 1}) : Lemma (i % 2 = 0) = assert(i % 2 = 0) by compute()

[@@ expect_failure]
let lemma_minus_two_mod_two (i: int{i = -2}) : Lemma (i % 2 = -1) = ()
[@@ expect_failure]
let lemma_minus_two_mod_two (i: int{i = -2}) : Lemma (i % 2 = -1) = assert(i % 2 = -1) by compute()

[briangmilnes]

let lemma_minus_one_div_two' = assert((-1) / 2 = -1) is worse, bug submitted.

[briangmilnes]

Nik says that this is Euclidean arithmetic and should be the answer to all above.
Testing this, it's right. Odd but right.