theorem MulOracleProof.csa64_main (a b : BitVec 64) : match Sparkle.Verification.MulProps.carrySaveN 64 0 0 a b with | (rd, rdx, fst, snd) => rd + rdx = a * b