Reference · Lemmas behind operations-research checks
rainbow.math.lemmas.fgt-order
General lemmas: fgt order. The mathematical facts the corresponding checks rest on, each checked by the kernel.
signed/fgt-clamp-bounds
signed/fgt-clamp-bounds : (fc-v fc-w : ℚ) → proposition/conjunction (0 ≤ data/Bool.rec (fun x₂₄ => ℚ) 0 fc-v (signed/decide-at-most 0 fc-v)) (proposition/conjunction (fc-v ≤ fc-w → 0 ≤ fc-w → data/Bool.rec (fun x₃₆ => ℚ) 0 fc-v (signed/decide-at-most 0 fc-v) ≤ fc-w) (fc-v ≤ 0 → data/Bool.rec (fun x₄₀ => ℚ) 0 fc-v (signed/decide-at-most 0 fc-v) = 0))
0 = signed/zero= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational≤ = signed/at-most
signed/fgt-gap-indicator
signed/fgt-gap-indicator : (gi-g gi-y gi-z : ℚ) (gi-hg : gi-g = data/Bool.rec (fun x₄ => ℚ) 0 (gi-z + signed/negate gi-y) (most)) (gi-hy : 0 ≤ gi-y) (gi-hz : 0 ≤ gi-z) → gi-g ≤ gi-z · data/Bool.rec (fun x₈ => ℚ) 1 0 (signed/decide-at-most gi-z gi-y) where most := signed/decide-at-most 0 (gi-z + signed/negate gi-y)
+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℚ = signed/SignedRational≤ = signed/at-most