theorem b1div2 (n: nat): $ b1 n // 2 = n $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | d1lt2 | 1 < 2 |
|
2 | 1 | a1i | T. -> 1 < 2 |
3 | b1mul21 | 2 * n + 1 = b1 n |
|
4 | 3 | a1i | T. -> 2 * n + 1 = b1 n |
5 | 2, 4 | eqdivmod | T. -> b1 n // 2 = n /\ b1 n % 2 = 1 |
6 | 5 | anld | T. -> b1 n // 2 = n |
7 | 6 | trud | b1 n // 2 = n |