a,b:
. a | b 
b | a a = 
ba,b:. |a| | |b| 
a | bx,y:. |x| = |y| x = ya,b:
. a | b b | a a = bP:(
Prop). (x:. P(|x|)) (x:. P(x))| Rank | Theorem | Name |
| 3 | a,b:. a | b b | a a = b | [divides_anti_sym] |
| cites the following: | ||
| 2 | a,b:. |a| | |b| a | b | [divides_of_absvals] |
| 0 | x,y:. |x| = |y| x = y | [absval_eq] |
| 2 | a,b:. a | b b | a a = b | [divides_anti_sym_n] |
| 0 | P:(Prop). (x:. P(|x|)) (x:. P(x)) | [absval_elim] |