theorem minS (a b: nat): $ suc (min a b) = min (suc a) (suc b) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
2 |
min a b + 1 = suc (min a b) |
||
5 |
min a b + 1 = min (a + 1) (b + 1) |
||
7 |
a + 1 = suc a |
||
8 |
T. -> a + 1 = suc a |
||
9 |
b + 1 = suc b |
||
10 |
T. -> b + 1 = suc b |
||
11 |
T. -> min (a + 1) (b + 1) = min (suc a) (suc b) |
||
12 |
min (a + 1) (b + 1) = min (suc a) (suc b) |
||
13 |
eqtr* |
min a b + 1 = min (suc a) (suc b) |
|
14 |
suc (min a b) = min (suc a) (suc b) |