theorem lelttr (a b c: nat): $ a <= b -> b < c -> a < c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lesuc | a <= b <-> suc a <= suc b |
|
2 | letr | suc a <= suc b -> suc b <= c -> suc a <= c |
|
3 | 2 | conv lt | suc a <= suc b -> b < c -> a < c |
4 | 1, 3 | sylbi | a <= b -> b < c -> a < c |