theorem ltled (G: wff) (a b: nat): $ G -> a < b $ > $ G -> a <= b $;
a < b -> a <= b
G -> a < b
G -> a <= b