At the level of derivability, we then have A ⊢ B iff δ(B) ⊢ δ(A): for every theorem or rule of NL, we also find its image under δ in LG. A note about the notation: we read B ⦸ A as ‘B from A’ and A ⊘ B as ‘A less B’, i.e., the quantity that is subtracted is put under the circled (back)slash, just as we have the denominator under the (back)slash in the case of left and right division types. In a formulas-as-types spirit, we will feel free to refer to the division operations also as implications, and to the difference operations as coimplications.