def CurveDivisor.IsEffective {C : Type u_1} (D : CurveDivisor C) : Prop

theorem CurveDivisor.isEffective_iff_nonneg {C : Type u_1} (D : CurveDivisor C) : D.IsEffective ↔ 0 ≤ D

theorem CurveDivisor.le_iff_isEffective_sub {C : Type u_1} (D₁ D₂ : CurveDivisor C) : D₁ ≤ D₂ ↔ (D₂ - D₁).IsEffective

theorem CurveDivisor.IsEffective.add {C : Type u_1} {D₁ D₂ : CurveDivisor C} (h₁ : D₁.IsEffective) (h₂ : D₂.IsEffective) : (D₁ + D₂).IsEffective

noncomputable def CurveDivisor.positivePart {C : Type u_1} (D : CurveDivisor C) : CurveDivisor C

noncomputable def CurveDivisor.negativePart {C : Type u_1} (D : CurveDivisor C) : CurveDivisor C

@[simp]

theorem CurveDivisor.positivePart_apply {C : Type u_1} (D : CurveDivisor C) (P : C) : D.positivePart P = max (D P) 0

@[simp]

theorem CurveDivisor.negativePart_apply {C : Type u_1} (D : CurveDivisor C) (P : C) : D.negativePart P = max (-D P) 0

theorem CurveDivisor.positivePart_isEffective {C : Type u_1} (D : CurveDivisor C) : D.positivePart.IsEffective

theorem CurveDivisor.decomposition {C : Type u_1} (D : CurveDivisor C) : D = D.positivePart - D.negativePart