def div_lt.go

lawful-words@0.1.0.0 · proof_nat.bend:1345

import Base

1345# a < b * c with b > 0 gives a / b < c.
1346def div_lt.go(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_lt(a, Nat.mul(b, c)) == True{} : Bool},
1347  t: Bool, et: {Nat.is_lt(Nat.div(a, b), c) == t : Bool}) -> {Nat.is_lt(Nat.div(a, b), c) == True{} : Bool}:
1348  match t:
1349    case True{}:
1350      et
1351    case False{}:
1352      +q = Nat.div(a, b)
1353      +hcq = not_lt_le(q, c, et)
1354      +hle = le_trans(Nat.mul(c, b), Nat.mul(q, b), a, le_mul_r(c, q, b, hcq),
1355        %div_mod(a, b) : {Nat.is_le(Nat.mul(q, b), _) == True{} : Bool}
1356        le_add_r(Nat.mul(q, b), Nat.mod(a, b)))
1357      +hlt = lt_le_trans(a, Nat.mul(b, c), a, h, %mul_comm(c, b) : {Nat.is_le(_, a) == True{} : Bool}; hle)
1358      Empty.absurd({Nat.is_lt(q, c) == True{} : Bool}, false_ne_true(
1359        Equal.trans(Bool, False{}, Nat.is_lt(a, a), True{}, Equal.sym(Bool, Nat.is_lt(a, a), False{}, lt_irrefl(a)), hlt)))