Logipedia
Modules
About
FAQ
Search
// This prints the left floatting menu
Dedukti
Matita
Coq
Lean
PVS
OpenTheory
Theorem
nat.le_plus_b
Statement
∀ b n m, (n + b) ≤ m ⇒ n ≤ m
Main Dependencies