theorem maxadd1 (a b c: nat): $ max a b + c = max (a + c) (b + c) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 |
a < b -> if (a < b) b a = b |
||
2 |
conv max |
a < b -> max a b = b |
|
3 |
a < b -> max a b + c = b + c |
||
4 |
a < b <-> a + c < b + c |
||
5 |
a + c < b + c -> if (a + c < b + c) (b + c) (a + c) = b + c |
||
6 |
conv max |
a + c < b + c -> max (a + c) (b + c) = b + c |
|
7 |
a < b -> max (a + c) (b + c) = b + c |
||
8 |
a < b -> max a b + c = max (a + c) (b + c) |
||
9 |
~a < b -> if (a < b) b a = a |
||
10 |
conv max |
~a < b -> max a b = a |
|
11 |
~a < b -> max a b + c = a + c |
||
13 |
~a < b <-> ~a + c < b + c |
||
14 |
~a + c < b + c -> if (a + c < b + c) (b + c) (a + c) = a + c |
||
15 |
conv max |
~a + c < b + c -> max (a + c) (b + c) = a + c |
|
16 |
~a < b -> max (a + c) (b + c) = a + c |
||
17 |
~a < b -> max a b + c = max (a + c) (b + c) |
||
18 |
max a b + c = max (a + c) (b + c) |