NaturalAddition.associative: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/natural_addition.bend as NaturalAddition
Lines 53-57 of stelliferous@0.0.2.0/proofs/natural_addition.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/natural_addition.bend&start_line=53&end_line=57

import Base

law associative:
  for +first: Nat
  for +second: Nat
  for +third: Nat
  {Nat.add(Nat.add(first,second),third) == Nat.add(first,Nat.add(second,third)) : Nat}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add