def aes_nat_eq_none_if_ne

qasim-bend-kit@0.1.0.2 · PROOF.bend:429

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

429def aes_nat_eq_none_if_ne(+a: Nat, +b: Nat,
430    no: {a != b : Nat}) ->
431    {AES.aes_nat_eq_proof(a, b) == None{} : Maybe<&0, {a == b : Nat}>}:
432    match a b:
433        case 0n 0n:
434            PrimitiveProof.absurd({AES.aes_nat_eq_proof(0n, 0n) == None{} :
435                Maybe<&0, {0n == 0n : Nat}>}, no({==}))
436        case 0n 1n+bp: {==}
437        case 1n+ap 0n: {==}
438        case 1n+ap 1n+bp:
439            recursive = aes_nat_eq_none_if_ne(ap, bp,
440                aes_nat_tail_ne(ap, bp, no))
441            Equal.trans(Maybe<&0, {1n+ap == 1n+bp : Nat}>,
442                AES.aes_nat_eq_step(ap, bp, AES.aes_nat_eq_proof(ap, bp)),
443                AES.aes_nat_eq_step(ap, bp, None{}), None{},
444                Equal.cong(Maybe<&0, {ap == bp : Nat}>,
445                    Maybe<&0, {1n+ap == 1n+bp : Nat}>,
446                    result => AES.aes_nat_eq_step(ap, bp, result),
447                    AES.aes_nat_eq_proof(ap, bp), None{}, recursive),
448                {==})