theorem letr (a b c: nat): $ a <= b -> b <= c -> a <= c $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anl | a <= b /\ b <= c -> a <= b |
|
| 2 | anr | a <= b /\ b <= c -> b <= c |
|
| 3 | 1, 2 | letrd | a <= b /\ b <= c -> a <= c |
| 4 | 3 | exp | a <= b -> b <= c -> a <= c |