def add_commutative

stelliferous@0.0.2.0 · proofs/bounded_u32_arithmetic.bend:36

import Base
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order

36def add_commutative(+left: U32,+right: U32) -> {(left + right : U32) == (right + left : U32) : U32}:
37  %Equal.sym(U32,(left + right : U32),U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))),native_add(left,right)) :
38    {_ == (right + left : U32) : U32}
39  %Equal.sym(U32,(right + left : U32),U32.from_nat(Nat.add(U32.to_nat(right),U32.to_nat(left))),native_add(right,left)) :
40    {U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))) == _ : U32}
41  %Order.commutative(U32.to_nat(left),U32.to_nat(right)) :
42    {U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))) == U32.from_nat(_) : U32}
43  {==}