def un.dd

bend-osdev-u32@0.1.0.0 · PROOF.bend:519

import Base

519# double R + double D, from R + D
520def un.dd(+r: Nat, +d: Nat, +a: Nat, +b: Nat, e: {Nat.add(r, d) == Nat.add(a, b) : Nat}) -> {Nat.add(Nat.double(r), Nat.double(d)) == Nat.add(Nat.double(a), Nat.double(b)) : Nat}:
521  Equal.trans(Nat, Nat.add(Nat.double(r), Nat.double(d)), Nat.double(Nat.add(r, d)), Nat.add(Nat.double(a), Nat.double(b)), Equal.sym(Nat, Nat.double(Nat.add(r, d)), Nat.add(Nat.double(r), Nat.double(d)), un.double_add(r, d)), Equal.trans(Nat, Nat.double(Nat.add(r, d)), Nat.double(Nat.add(a, b)), Nat.add(Nat.double(a), Nat.double(b)), un.double_cong(Nat.add(r, d), Nat.add(a, b), e), un.double_add(a, b)))