NaturalAddition.zero_right: law of stelliferous@0.0.2.0 Import: import stelliferous@0.0.2.0/proofs/natural_addition.bend as NaturalAddition Lines 30-32 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=30&end_line=32 import Base law zero_right: for +n: Nat {Nat.add(n,0n) == n : Nat} Uses (2): 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