def key_succ.conclusion

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

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

54def key_succ.conclusion(+d: Nat, +e: Nat, +i: Nat, +j: Nat, p: {Q.le.same(Nat.is_eq(d, e), i, j, d, e) == True{} : Bool}) -> {Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e) == True{} : Bool}:
55  Equal.trans(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), True{}, key_succ(Nat.is_eq(d, e), i, j, d, e), p)