def lt_mul_cancel.go

lawful-words@0.1.0.0 · proof_nat.bend:1553

import Base

1553# 8a < 8b gives a < b.
1554def lt_mul_cancel.go(+c: Nat, +a: Nat, +b: Nat, +h: {Nat.is_lt(Nat.mul(c, a), Nat.mul(c, b)) == True{} : Bool},
1555  t: Bool, et: {Nat.is_lt(a, b) == t : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
1556  match t:
1557    case True{}:
1558      et
1559    case False{}:
1560      Empty.absurd({Nat.is_lt(a, b) == True{} : Bool}, false_ne_true(
1561        Equal.trans(Bool, False{}, Nat.is_lt(Nat.mul(c, a), Nat.mul(c, a)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.mul(c, a), Nat.mul(c, a)), False{}, lt_irrefl(Nat.mul(c, a))),
1562          lt_le_trans(Nat.mul(c, a), Nat.mul(c, b), Nat.mul(c, a), h, le_mul_l(c, b, a, not_lt_le(a, b, et))))))