law le_add_mono_l
import lawful-words@0.1.0.0/proof_nat.bend as ProofNatimport Base
856law le_add_mono_l:
857 for +c: Nat
858 for +a: Nat
859 for +b: Nat
860 for h: {Nat.is_le(a, b) == True{} : Bool}
861 {Nat.is_le(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}