def key_succ.premise

bend-kit-scheduler@0.4.1.0 · queue_proof.bend:51

import Base
import bend-kit-scheduler@0.4.1.0/queue.bend as Q

51def key_succ.premise(+d: Nat, +e: Nat, +i: Nat, +j: Nat, +b: Bool, p: {Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e) == b : Bool}) -> {Q.le.same(Nat.is_eq(d, e), i, j, d, e) == b : Bool}:
52  Equal.trans(Bool, Q.le.same(Nat.is_eq(d, e), i, j, d, e), Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e), b, Equal.sym(Bool, Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e), Q.le.same(Nat.is_eq(d, e), i, j, d, e), key_succ(Nat.is_eq(d, e), i, j, d, e)), p)