Description: A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | divscan2wd.1 | |
|
divscan2wd.2 | |
||
divscan2wd.3 | |
||
divscan2wd.4 | |
||
Assertion | divscan2wd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | divscan2wd.1 | |
|
2 | divscan2wd.2 | |
|
3 | divscan2wd.3 | |
|
4 | divscan2wd.4 | |
|
5 | eqid | |
|
6 | 1 2 3 4 | divsclwd | |
7 | 1 6 2 3 4 | divsmulwd | |
8 | 5 7 | mpbii | |