def wm.k

bend-osdev-word64@0.1.1.0 · PROOF_mul.bend:254

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

254def wm.k(+n: Nat, +h: Nat, +A: Nat, +B: Nat, +X0: Nat, +X1: Nat, +Y0: Nat, +Y1: Nat, +P00: Nat, +P01: Nat, +P10: Nat, +P11: Nat, +S00: Nat, +L01: Nat, +L10: Nat, +M1: Nat, +MID: Nat, +H01: Nat, +H10: Nat, +HM: Nat, +T1: Nat, +T2: Nat, +HI: Nat, +LO: Nat, +C1: Nat, +C2: Nat, +C3: Nat, +C4: Nat, +C5: Nat, +en: {Nat.add(h, h) == n : Nat}, +h2: {Nat.is_le(2n, h) == True{} : Bool}, +hA: {Nat.is_lt(A, U.U32Nat.dbl(n, 1n)) == True{} : Bool}, +hB: {Nat.is_lt(B, U.U32Nat.dbl(n, 1n)) == True{} : Bool}, +eX0: {X0 == U.U32Nat.low(h, A) : Nat}, +eX1: {X1 == U.U32Nat.high(h, A) : Nat}, +eY0: {Y0 == U.U32Nat.low(h, B) : Nat}, +eY1: {Y1 == U.U32Nat.high(h, B) : Nat}, +e00: {P00 == U.U32Nat.low(n, Nat.mul(X0, Y0)) : Nat}, +e01: {P01 == U.U32Nat.low(n, Nat.mul(X0, Y1)) : Nat}, +e10: {P10 == U.U32Nat.low(n, Nat.mul(X1, Y0)) : Nat}, +e11: {P11 == U.U32Nat.low(n, Nat.mul(X1, Y1)) : Nat}, +eS: {S00 == U.U32Nat.high(h, P00) : Nat}, +eL1: {L01 == U.U32Nat.low(h, P01) : Nat}, +eL2: {L10 == U.U32Nat.low(h, P10) : Nat}, +eM1: {Nat.add(M1, U.U32Nat.dbl(n, C1)) == Nat.add(S00, L01) : Nat}, +eMID: {Nat.add(MID, U.U32Nat.dbl(n, C2)) == Nat.add(M1, L10) : Nat}, +eH1: {H01 == U.U32Nat.high(h, P01) : Nat}, +eH2: {H10 == U.U32Nat.high(h, P10) : Nat}, +eHM: {HM == U.U32Nat.high(h, MID) : Nat}, +eT1: {Nat.add(T1, U.U32Nat.dbl(n, C3)) == Nat.add(P11, H01) : Nat}, +eT2: {Nat.add(T2, U.U32Nat.dbl(n, C4)) == Nat.add(T1, H10) : Nat}, +eHI: {Nat.add(HI, U.U32Nat.dbl(n, C5)) == Nat.add(T2, HM) : Nat}, +eLO: {LO == U.U32Nat.low(n, Nat.mul(A, B)) : Nat}) -> {Nat.add(LO, U.U32Nat.dbl(n, HI)) == Nat.mul(A, B) : Nat}:
255  +hx0 = Equal.trans(Bool, Nat.is_lt(X0, U.U32Nat.dbl(h, 1n)), Nat.is_lt(U.U32Nat.low(h, A), U.U32Nat.dbl(h, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(h, 1n)), X0, U.U32Nat.low(h, A), Equal.sym(Nat, U.U32Nat.low(h, A), X0, Equal.sym(Nat, X0, U.U32Nat.low(h, A), eX0))), UL.low_lt(h, A))
256  +hy0 = Equal.trans(Bool, Nat.is_lt(Y0, U.U32Nat.dbl(h, 1n)), Nat.is_lt(U.U32Nat.low(h, B), U.U32Nat.dbl(h, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(h, 1n)), Y0, U.U32Nat.low(h, B), Equal.sym(Nat, U.U32Nat.low(h, B), Y0, Equal.sym(Nat, Y0, U.U32Nat.low(h, B), eY0))), UL.low_lt(h, B))
257  +hx1 = Equal.trans(Bool, Nat.is_lt(X1, U.U32Nat.dbl(h, 1n)), Nat.is_lt(U.U32Nat.high(h, A), U.U32Nat.dbl(h, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(h, 1n)), X1, U.U32Nat.high(h, A), Equal.sym(Nat, U.U32Nat.high(h, A), X1, Equal.sym(Nat, X1, U.U32Nat.high(h, A), eX1))), wm.hl(h, A, U.U32Nat.dbl(h, 1n), Equal.trans(Bool, Nat.is_lt(A, U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n))), Nat.is_lt(A, U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(A, zz), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), U.U32Nat.dbl(n, 1n), Equal.sym(Nat, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), wm.fn(h, n, 1n, en))), hA)))
258  +hy1 = Equal.trans(Bool, Nat.is_lt(Y1, U.U32Nat.dbl(h, 1n)), Nat.is_lt(U.U32Nat.high(h, B), U.U32Nat.dbl(h, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(h, 1n)), Y1, U.U32Nat.high(h, B), Equal.sym(Nat, U.U32Nat.high(h, B), Y1, Equal.sym(Nat, Y1, U.U32Nat.high(h, B), eY1))), wm.hl(h, B, U.U32Nat.dbl(h, 1n), Equal.trans(Bool, Nat.is_lt(B, U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n))), Nat.is_lt(B, U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(B, zz), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), U.U32Nat.dbl(n, 1n), Equal.sym(Nat, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), wm.fn(h, n, 1n, en))), hB)))
259  +pl00 = wm.pl(h, n, X0, Y0, en, hx0, hy0)
260  +pe00 = Equal.trans(Nat, P00, U.U32Nat.low(n, Nat.mul(X0, Y0)), Nat.mul(X0, Y0), e00, UL.low_small(n, Nat.mul(X0, Y0), pl00))
261  +plt00 = Equal.trans(Bool, Nat.is_lt(P00, U.U32Nat.dbl(n, 1n)), Nat.is_lt(Nat.mul(X0, Y0), U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(n, 1n)), P00, Nat.mul(X0, Y0), Equal.sym(Nat, Nat.mul(X0, Y0), P00, Equal.sym(Nat, P00, Nat.mul(X0, Y0), pe00))), pl00)
262  +pl01 = wm.pl(h, n, X0, Y1, en, hx0, hy1)
263  +pe01 = Equal.trans(Nat, P01, U.U32Nat.low(n, Nat.mul(X0, Y1)), Nat.mul(X0, Y1), e01, UL.low_small(n, Nat.mul(X0, Y1), pl01))
264  +plt01 = Equal.trans(Bool, Nat.is_lt(P01, U.U32Nat.dbl(n, 1n)), Nat.is_lt(Nat.mul(X0, Y1), U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(n, 1n)), P01, Nat.mul(X0, Y1), Equal.sym(Nat, Nat.mul(X0, Y1), P01, Equal.sym(Nat, P01, Nat.mul(X0, Y1), pe01))), pl01)
265  +pl10 = wm.pl(h, n, X1, Y0, en, hx1, hy0)
266  +pe10 = Equal.trans(Nat, P10, U.U32Nat.low(n, Nat.mul(X1, Y0)), Nat.mul(X1, Y0), e10, UL.low_small(n, Nat.mul(X1, Y0), pl10))
267  +plt10 = Equal.trans(Bool, Nat.is_lt(P10, U.U32Nat.dbl(n, 1n)), Nat.is_lt(Nat.mul(X1, Y0), U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(n, 1n)), P10, Nat.mul(X1, Y0), Equal.sym(Nat, Nat.mul(X1, Y0), P10, Equal.sym(Nat, P10, Nat.mul(X1, Y0), pe10))), pl10)
268  +pl11 = wm.pl(h, n, X1, Y1, en, hx1, hy1)
269  +pe11 = Equal.trans(Nat, P11, U.U32Nat.low(n, Nat.mul(X1, Y1)), Nat.mul(X1, Y1), e11, UL.low_small(n, Nat.mul(X1, Y1), pl11))
270  +plt11 = Equal.trans(Bool, Nat.is_lt(P11, U.U32Nat.dbl(n, 1n)), Nat.is_lt(Nat.mul(X1, Y1), U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(n, 1n)), P11, Nat.mul(X1, Y1), Equal.sym(Nat, Nat.mul(X1, Y1), P11, Equal.sym(Nat, P11, Nat.mul(X1, Y1), pe11))), pl11)
271  +hS = Equal.trans(Bool, Nat.is_lt(S00, U.U32Nat.dbl(h, 1n)), Nat.is_lt(U.U32Nat.high(h, P00), U.U32Nat.dbl(h, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(h, 1n)), S00, U.U32Nat.high(h, P00), Equal.sym(Nat, U.U32Nat.high(h, P00), S00, Equal.sym(Nat, S00, U.U32Nat.high(h, P00), eS))), wm.hl(h, P00, U.U32Nat.dbl(h, 1n), Equal.trans(Bool, Nat.is_lt(P00, U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n))), Nat.is_lt(P00, U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(P00, zz), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), U.U32Nat.dbl(n, 1n), Equal.sym(Nat, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), wm.fn(h, n, 1n, en))), plt00)))
272  +hL1 = Equal.trans(Bool, Nat.is_lt(L01, U.U32Nat.dbl(h, 1n)), Nat.is_lt(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(h, 1n)), L01, U.U32Nat.low(h, P01), Equal.sym(Nat, U.U32Nat.low(h, P01), L01, Equal.sym(Nat, L01, U.U32Nat.low(h, P01), eL1))), UL.low_lt(h, P01))
273  +hL2 = Equal.trans(Bool, Nat.is_lt(L10, U.U32Nat.dbl(h, 1n)), Nat.is_lt(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(h, 1n)), L10, U.U32Nat.low(h, P10), Equal.sym(Nat, U.U32Nat.low(h, P10), L10, Equal.sym(Nat, L10, U.U32Nat.low(h, P10), eL2))), UL.low_lt(h, P10))
274  +s3lt = wm.s3(h, n, S00, L01, L10, en, h2, hS, hL1, hL2)
275  +em1 = UL.dbl_nowrap(n, C1, M1, Nat.add(S00, L01), Nat.add(Nat.add(S00, L01), L10), eM1, Equal.trans(Bool, Nat.is_le(Nat.add(S00, L01), Nat.add(Nat.add(S00, L01), L10)), Nat.is_le(Nat.add(S00, L01), Nat.add(L10, Nat.add(S00, L01))), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(S00, L01), Nat.add(L10, Nat.add(S00, L01))), Nat.is_le(Nat.add(S00, L01), Nat.add(Nat.add(S00, L01), L10)), Equal.cong(Nat, Bool, zz => Nat.is_le(Nat.add(S00, L01), zz), Nat.add(L10, Nat.add(S00, L01)), Nat.add(Nat.add(S00, L01), L10), wr.m4(L10, S00, L01))), UL.nat_le_add(Nat.add(S00, L01), L10)), s3lt)
276  +emid = Equal.trans(Nat, MID, Nat.add(M1, L10), Nat.add(Nat.add(S00, L01), L10), UL.dbl_nowrap(n, C2, MID, Nat.add(M1, L10), Nat.add(Nat.add(S00, L01), L10), eMID, Equal.trans(Bool, Nat.is_le(Nat.add(M1, L10), Nat.add(Nat.add(S00, L01), L10)), Nat.is_le(Nat.add(Nat.add(S00, L01), L10), Nat.add(Nat.add(S00, L01), L10)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_le(zz, Nat.add(Nat.add(S00, L01), L10)), Nat.add(M1, L10), Nat.add(Nat.add(S00, L01), L10), Equal.cong(Nat, Nat, zz => Nat.add(zz, L10), M1, Nat.add(S00, L01), em1)), UL.nat_le_refl(Nat.add(Nat.add(S00, L01), L10))), s3lt), Equal.cong(Nat, Nat, zz => Nat.add(zz, L10), M1, Nat.add(S00, L01), em1))
277  +eE = Equal.trans(Nat, Nat.mul(A, B), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.low(h, MID))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)))), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.low(h, MID))), U.U32Nat.dbl(n, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, Nat.add(U.U32Nat.low(h, MID), U.U32Nat.dbl(h, HM))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.low(h, MID))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, Nat.add(U.U32Nat.low(h, MID), U.U32Nat.dbl(h, U.U32Nat.high(h, MID)))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, Nat.add(U.U32Nat.low(h, MID), U.U32Nat.dbl(h, HM))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, MID), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, Nat.add(U.U32Nat.low(h, MID), U.U32Nat.dbl(h, U.U32Nat.high(h, MID)))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(S00, L01), L10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, MID), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, H01)), Nat.add(L10, U.U32Nat.dbl(h, H10)))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(S00, L01), L10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, H01)), Nat.add(L10, U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, H01)), Nat.add(L10, U.U32Nat.dbl(h, H10)))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, H01)), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, H01)), Nat.add(L10, U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, H01)), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.high(h, P00))), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.high(h, P00))), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.high(h, P00))), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.high(h, P00))), Nat.add(U.U32Nat.dbl(h, Nat.add(P01, P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.high(h, P00))), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(P01, P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.high(h, P00))), Nat.add(U.U32Nat.dbl(h, Nat.add(P01, P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(P01, P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(P01, P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(P01, Nat.mul(X1, Y0))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(P01, P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.mul(X0, Y1), Nat.mul(X1, Y0))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(P01, Nat.mul(X1, Y0))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Equal.trans(Nat, Nat.mul(A, B), Nat.add(Nat.mul(X0, Y0), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.mul(X0, Y1), Nat.mul(X1, Y0))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.mul(X0, Y1), Nat.mul(X1, Y0))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Equal.trans(Nat, Nat.mul(A, B), Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, X1)), Nat.add(Y0, U.U32Nat.dbl(h, Y1))), Nat.add(Nat.mul(X0, Y0), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.mul(X0, Y1), Nat.mul(X1, Y0))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Equal.trans(Nat, Nat.mul(A, B), Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, X1)), Nat.add(Y0, U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, X1)), Nat.add(Y0, U.U32Nat.dbl(h, Y1))), Equal.trans(Nat, Nat.mul(A, B), Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, X1)), Nat.add(U.U32Nat.low(h, B), U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, X1)), Nat.add(Y0, U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), Equal.trans(Nat, Nat.mul(A, B), Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, U.U32Nat.high(h, A))), Nat.add(U.U32Nat.low(h, B), U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, X1)), Nat.add(U.U32Nat.low(h, B), U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), Equal.trans(Nat, Nat.mul(A, B), Nat.mul(Nat.add(U.U32Nat.low(h, A), U.U32Nat.dbl(h, U.U32Nat.high(h, A))), Nat.add(U.U32Nat.low(h, B), U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, U.U32Nat.high(h, A))), Nat.add(U.U32Nat.low(h, B), U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), Equal.trans(Nat, Nat.mul(A, B), Nat.mul(Nat.add(U.U32Nat.low(h, A), U.U32Nat.dbl(h, U.U32Nat.high(h, A))), B), Nat.mul(Nat.add(U.U32Nat.low(h, A), U.U32Nat.dbl(h, U.U32Nat.high(h, A))), Nat.add(U.U32Nat.low(h, B), U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), Equal.cong(Nat, Nat, zz => Nat.mul(zz, B), A, Nat.add(U.U32Nat.low(h, A), U.U32Nat.dbl(h, U.U32Nat.high(h, A))), Equal.sym(Nat, Nat.add(U.U32Nat.low(h, A), U.U32Nat.dbl(h, U.U32Nat.high(h, A))), A, UL.low_high(h, A))), Equal.cong(Nat, Nat, zz => Nat.mul(Nat.add(U.U32Nat.low(h, A), U.U32Nat.dbl(h, U.U32Nat.high(h, A))), zz), B, Nat.add(U.U32Nat.low(h, B), U.U32Nat.dbl(h, U.U32Nat.high(h, B))), Equal.sym(Nat, Nat.add(U.U32Nat.low(h, B), U.U32Nat.dbl(h, U.U32Nat.high(h, B))), B, UL.low_high(h, B)))), Equal.cong(Nat, Nat, zz => Nat.mul(Nat.add(zz, U.U32Nat.dbl(h, U.U32Nat.high(h, A))), Nat.add(U.U32Nat.low(h, B), U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), U.U32Nat.low(h, A), X0, Equal.sym(Nat, X0, U.U32Nat.low(h, A), eX0))), Equal.cong(Nat, Nat, zz => Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, zz)), Nat.add(U.U32Nat.low(h, B), U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), U.U32Nat.high(h, A), X1, Equal.sym(Nat, X1, U.U32Nat.high(h, A), eX1))), Equal.cong(Nat, Nat, zz => Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, X1)), Nat.add(zz, U.U32Nat.dbl(h, U.U32Nat.high(h, B)))), U.U32Nat.low(h, B), Y0, Equal.sym(Nat, Y0, U.U32Nat.low(h, B), eY0))), Equal.cong(Nat, Nat, zz => Nat.mul(Nat.add(X0, U.U32Nat.dbl(h, X1)), Nat.add(Y0, U.U32Nat.dbl(h, zz))), U.U32Nat.high(h, B), Y1, Equal.sym(Nat, Y1, U.U32Nat.high(h, B), eY1))), wr.m5(X0, h, X1, Y0, Y1)), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.mul(X0, Y1), Nat.mul(X1, Y0))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Nat.mul(X0, Y0), P00, Equal.sym(Nat, P00, Nat.mul(X0, Y0), pe00))), Equal.cong(Nat, Nat, zz => Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(zz, Nat.mul(X1, Y0))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Nat.mul(X0, Y1), P01, Equal.sym(Nat, P01, Nat.mul(X0, Y1), pe01))), Equal.cong(Nat, Nat, zz => Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(P01, zz)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.mul(X1, Y1))))), Nat.mul(X1, Y0), P10, Equal.sym(Nat, P10, Nat.mul(X1, Y0), pe10))), Equal.cong(Nat, Nat, zz => Nat.add(P00, Nat.add(U.U32Nat.dbl(h, Nat.add(P01, P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, zz)))), Nat.mul(X1, Y1), P11, Equal.sym(Nat, P11, Nat.mul(X1, Y1), pe11))), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.add(U.U32Nat.dbl(h, Nat.add(P01, P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), P00, Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.high(h, P00))), Equal.sym(Nat, Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.high(h, P00))), P00, UL.low_high(h, P00)))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.high(h, P00))), Nat.add(U.U32Nat.dbl(h, Nat.add(zz, P10)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), P01, Nat.add(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), Equal.sym(Nat, Nat.add(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), P01, UL.low_high(h, P01)))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.high(h, P00))), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), zz)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), P10, Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))), Equal.sym(Nat, Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))), P10, UL.low_high(h, P10)))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, zz)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(U.U32Nat.low(h, P01), U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), U.U32Nat.high(h, P00), S00, Equal.sym(Nat, S00, U.U32Nat.high(h, P00), eS))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(zz, U.U32Nat.dbl(h, U.U32Nat.high(h, P01))), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), U.U32Nat.low(h, P01), L01, Equal.sym(Nat, L01, U.U32Nat.low(h, P01), eL1))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, zz)), Nat.add(U.U32Nat.low(h, P10), U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), U.U32Nat.high(h, P01), H01, Equal.sym(Nat, H01, U.U32Nat.high(h, P01), eH1))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, H01)), Nat.add(zz, U.U32Nat.dbl(h, U.U32Nat.high(h, P10))))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), U.U32Nat.low(h, P10), L10, Equal.sym(Nat, L10, U.U32Nat.low(h, P10), eL2))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, S00)), Nat.add(U.U32Nat.dbl(h, Nat.add(Nat.add(L01, U.U32Nat.dbl(h, H01)), Nat.add(L10, U.U32Nat.dbl(h, zz)))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, P11)))), U.U32Nat.high(h, P10), H10, Equal.sym(Nat, H10, U.U32Nat.high(h, P10), eH2))), wr.m6(U.U32Nat.low(h, P00), h, S00, L01, H01, L10, H10, P11)), Equal.cong(Nat, Nat, zz => Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, zz), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), Nat.add(Nat.add(S00, L01), L10), MID, Equal.sym(Nat, MID, Nat.add(Nat.add(S00, L01), L10), emid))), Equal.cong(Nat, Nat, zz => Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, zz), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), MID, Nat.add(U.U32Nat.low(h, MID), U.U32Nat.dbl(h, U.U32Nat.high(h, MID))), Equal.sym(Nat, Nat.add(U.U32Nat.low(h, MID), U.U32Nat.dbl(h, U.U32Nat.high(h, MID))), MID, UL.low_high(h, MID)))), Equal.cong(Nat, Nat, zz => Nat.add(U.U32Nat.low(h, P00), Nat.add(U.U32Nat.dbl(h, Nat.add(U.U32Nat.low(h, MID), U.U32Nat.dbl(h, zz))), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(P11, H01), H10))))), U.U32Nat.high(h, MID), HM, Equal.sym(Nat, HM, U.U32Nat.high(h, MID), eHM))), wr.m7(U.U32Nat.low(h, P00), h, U.U32Nat.low(h, MID), HM, P11, H01, H10)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.low(h, MID))), zz), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM))), U.U32Nat.dbl(n, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), Equal.sym(Nat, U.U32Nat.dbl(n, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), U.U32Nat.dbl(h, U.U32Nat.dbl(h, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM))), wm.fn(h, n, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), en))))
278  +lowlt = wm.low2(h, n, U.U32Nat.low(h, P00), U.U32Nat.low(h, MID), en, UL.low_lt(h, P00), UL.low_lt(h, MID))
279  +ehi = UL.high_unique(n, Nat.mul(A, B), Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.low(h, MID))), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), Equal.sym(Nat, Nat.mul(A, B), Nat.add(Nat.add(U.U32Nat.low(h, P00), U.U32Nat.dbl(h, U.U32Nat.low(h, MID))), U.U32Nat.dbl(n, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM))), eE), lowlt)
280  +hilt = Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), U.U32Nat.dbl(n, 1n)), Nat.is_lt(U.U32Nat.high(n, Nat.mul(A, B)), U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(n, 1n)), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), U.U32Nat.high(n, Nat.mul(A, B)), Equal.sym(Nat, U.U32Nat.high(n, Nat.mul(A, B)), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), U.U32Nat.high(n, Nat.mul(A, B)), ehi))), wm.hl(n, Nat.mul(A, B), U.U32Nat.dbl(n, 1n), Equal.trans(Bool, Nat.is_lt(Nat.mul(A, B), U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n))), Nat.is_lt(Nat.mul(A, B), Nat.mul(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n))), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(Nat.mul(A, B), zz), U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n)), Nat.mul(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n)), Equal.sym(Nat, Nat.mul(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n)), U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n)), wr.m3(n))), UL.nat_mul_lt(A, B, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n), hA, hB))))
281  +et1 = UL.dbl_nowrap(n, C3, T1, Nat.add(P11, H01), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), eT1, Equal.trans(Bool, Nat.is_le(Nat.add(P11, H01), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), Nat.is_le(Nat.add(P11, H01), Nat.add(Nat.add(H10, HM), Nat.add(P11, H01))), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(P11, H01), Nat.add(Nat.add(H10, HM), Nat.add(P11, H01))), Nat.is_le(Nat.add(P11, H01), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), Equal.cong(Nat, Bool, zz => Nat.is_le(Nat.add(P11, H01), zz), Nat.add(Nat.add(H10, HM), Nat.add(P11, H01)), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), wr.m8(H10, HM, P11, H01))), UL.nat_le_add(Nat.add(P11, H01), Nat.add(H10, HM))), hilt)
282  +et2 = Equal.trans(Nat, T2, Nat.add(T1, H10), Nat.add(Nat.add(P11, H01), H10), UL.dbl_nowrap(n, C4, T2, Nat.add(T1, H10), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), eT2, Equal.trans(Bool, Nat.is_le(Nat.add(T1, H10), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), Nat.is_le(Nat.add(Nat.add(P11, H01), H10), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_le(zz, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), Nat.add(T1, H10), Nat.add(Nat.add(P11, H01), H10), Equal.cong(Nat, Nat, zz => Nat.add(zz, H10), T1, Nat.add(P11, H01), et1)), Equal.trans(Bool, Nat.is_le(Nat.add(Nat.add(P11, H01), H10), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), Nat.is_le(Nat.add(Nat.add(P11, H01), H10), Nat.add(HM, Nat.add(Nat.add(P11, H01), H10))), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(Nat.add(P11, H01), H10), Nat.add(HM, Nat.add(Nat.add(P11, H01), H10))), Nat.is_le(Nat.add(Nat.add(P11, H01), H10), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), Equal.cong(Nat, Bool, zz => Nat.is_le(Nat.add(Nat.add(P11, H01), H10), zz), Nat.add(HM, Nat.add(Nat.add(P11, H01), H10)), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), wr.m9(HM, P11, H01, H10))), UL.nat_le_add(Nat.add(Nat.add(P11, H01), H10), HM))), hilt), Equal.cong(Nat, Nat, zz => Nat.add(zz, H10), T1, Nat.add(P11, H01), et1))
283  +ehi2 = Equal.trans(Nat, HI, Nat.add(T2, HM), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), UL.dbl_nowrap(n, C5, HI, Nat.add(T2, HM), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), eHI, Equal.trans(Bool, Nat.is_le(Nat.add(T2, HM), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), Nat.is_le(Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_le(zz, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM)), Nat.add(T2, HM), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), Equal.cong(Nat, Nat, zz => Nat.add(zz, HM), T2, Nat.add(Nat.add(P11, H01), H10), et2)), UL.nat_le_refl(Nat.add(Nat.add(Nat.add(P11, H01), H10), HM))), hilt), Equal.cong(Nat, Nat, zz => Nat.add(zz, HM), T2, Nat.add(Nat.add(P11, H01), H10), et2))
284  Equal.trans(Nat, Nat.add(LO, U.U32Nat.dbl(n, HI)), Nat.add(U.U32Nat.low(n, Nat.mul(A, B)), U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(A, B)))), Nat.mul(A, B), Equal.trans(Nat, Nat.add(LO, U.U32Nat.dbl(n, HI)), Nat.add(U.U32Nat.low(n, Nat.mul(A, B)), U.U32Nat.dbl(n, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM))), Nat.add(U.U32Nat.low(n, Nat.mul(A, B)), U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(A, B)))), Equal.trans(Nat, Nat.add(LO, U.U32Nat.dbl(n, HI)), Nat.add(U.U32Nat.low(n, Nat.mul(A, B)), U.U32Nat.dbl(n, HI)), Nat.add(U.U32Nat.low(n, Nat.mul(A, B)), U.U32Nat.dbl(n, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM))), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(n, HI)), LO, U.U32Nat.low(n, Nat.mul(A, B)), eLO), Equal.cong(Nat, Nat, zz => Nat.add(U.U32Nat.low(n, Nat.mul(A, B)), U.U32Nat.dbl(n, zz)), HI, Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), ehi2)), Equal.cong(Nat, Nat, zz => Nat.add(U.U32Nat.low(n, Nat.mul(A, B)), U.U32Nat.dbl(n, zz)), Nat.add(Nat.add(Nat.add(P11, H01), H10), HM), U.U32Nat.high(n, Nat.mul(A, B)), ehi)), UL.low_high(n, Nat.mul(A, B)))