def contra

bend-kit-collections@0.1.4.1 · nat_order.bend:156

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat

156# A combined hypothesis F(p) <= F(q) with q < p term by term is false.
157def contra(+p: Lin, q: Lin, v: Vs, e: LE(F(p, v), F(q, v)), h: {lle(lsuc(q), p) == True{} : Bool}) -> Empty:
158  match q v:
159    case L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
160      +vs = {VS{v1, v2, v3, v4} : Vs}
161      +fq = F(L{b0, b1, b2, b3, b4}, vs)
162      le_succ_false(fq, MNat.le_trans(1n+fq, F(p, vs), fq, F_mono(L{1n+b0, b1, b2, b3, b4}, p, vs, h), e))