theorem ltle (a b: nat): $ a < b -> a <= b $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lesucid | a <= suc a |
|
2 | 1 | a1i | a < b -> a <= suc a |
3 | id | a < b -> a < b |
|
4 | 3 | conv lt | a < b -> suc a <= b |
5 | 2, 4 | letrd | a < b -> a <= b |