a,b,c:
. a
b = c 
((a
b) ~ c)0) 
(
A)a,b:
, B:({a..b
}
Type).
Thm* a<b
((i:{a..b}B(i)) ~ ((i:{a..(b-1)}B(i))+B(b-1)))i1,i2,j1,j2:. i1
j1 i2j2 i1i2j1j2c,a,b:. a+b = c ((a+b) ~ c)| Rank | Theorem | Name |
| 7 | a,b,c:. ab = c ((ab) ~ c) | [nsub_mul] |
| cites the following: | ||
| 0 | 0) (A) | [card0_iff_uninhabited] |
| 6 | a,b:, B:({a..b}Type).
Thm* a<b ((i:{a..b}B(i)) ~ ((i:{a..(b-1)}B(i))+B(b-1))) | [card_split_end_sum_intseg_family] |
| 1 | i1,i2,j1,j2:. i1j1 i2j2 i1i2j1j2 | [multiply_functionality_wrt_le] |
| 5 | c,a,b:. a+b = c ((a+b) ~ c) | [nsub_add] |