def mod_le_sub

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:80

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR2

80# b mod r + r <= b for 0 < r <= b (the quotient is at least 1)
81def mod_le_sub(+b: Nat, +rp: Nat, +h: {Nat.is_le(1n+rp, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(Nat.mod(b, 1n+rp), 1n+rp), b) == True{} : Bool}:
82  +q = Nat.div(b, 1n+rp)
83  +m = Nat.mod(b, 1n+rp)
84  +e = NR.dm_eq(rp, b)
85  +m1 = Equal.trans(Nat, Nat.mul(1n, 1n+rp), Nat.add(1n+rp, 0n), 1n+rp, {==}, N.add_zero(1n+rp))
86  +hq = Equal.trans(Bool, Nat.is_le(1n, q), Nat.is_le(Nat.mul(1n, 1n+rp), b), True{}, NR.le_div(rp, 1n, b), L.subst(Nat, z => {Nat.is_le(z, b) == True{} : Bool}, 1n+rp, Nat.mul(1n, 1n+rp), Equal.sym(Nat, Nat.mul(1n, 1n+rp), 1n+rp, m1), h))
87  +le1 = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(q, 1n+rp)) == True{} : Bool}, Nat.mul(1n, 1n+rp), 1n+rp, m1, AR2.mul_le(1n, q, 1n+rp, hq))
88  +le2 = N.le_add_left(1n+rp, Nat.mul(q, 1n+rp), m, le1)
89  +le3 = L.subst(Nat, z => {Nat.is_le(Nat.add(m, 1n+rp), z) == True{} : Bool}, Nat.add(m, Nat.mul(q, 1n+rp)), b, Equal.trans(Nat, Nat.add(m, Nat.mul(q, 1n+rp)), Nat.add(Nat.mul(q, 1n+rp), m), b, NA.add_comm(m, Nat.mul(q, 1n+rp)), Equal.sym(Nat, b, Nat.add(Nat.mul(q, 1n+rp), m), e)), le2)
90  le3