PROOF.aes_nat_eq_none_if_ne: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/PROOF.bend as PROOF
Lines 429-448 of qasim-bend-kit@0.1.0.2/PROOF.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/PROOF.bend&start_line=429&end_line=448

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend as PrimitiveProof

def aes_nat_eq_none_if_ne(+a: Nat, +b: Nat,
    no: {a != b : Nat}) ->
    {AES.aes_nat_eq_proof(a, b) == None{} : Maybe<&0, {a == b : Nat}>}:
    match a b:
        case 0n 0n:
            PrimitiveProof.absurd({AES.aes_nat_eq_proof(0n, 0n) == None{} :
                Maybe<&0, {0n == 0n : Nat}>}, no({==}))
        case 0n 1n+bp: {==}
        case 1n+ap 0n: {==}
        case 1n+ap 1n+bp:
            recursive = aes_nat_eq_none_if_ne(ap, bp,
                aes_nat_tail_ne(ap, bp, no))
            Equal.trans(Maybe<&0, {1n+ap == 1n+bp : Nat}>,
                AES.aes_nat_eq_step(ap, bp, AES.aes_nat_eq_proof(ap, bp)),
                AES.aes_nat_eq_step(ap, bp, None{}), None{},
                Equal.cong(Maybe<&0, {ap == bp : Nat}>,
                    Maybe<&0, {1n+ap == 1n+bp : Nat}>,
                    result => AES.aes_nat_eq_step(ap, bp, result),
                    AES.aes_nat_eq_proof(ap, bp), None{}, recursive),
                {==})

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/PROOF.bend&name=aes_nat_tail_ne
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=aes_nat_eq_proof
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=aes_nat_eq_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=absurd