proposition: Lemma cut_minus_plus_distr x₁ x₂ y₁ y₂ : y₁ ≤ x₁ → y₂ ≤ x₂ → (x₁ ∸ y₁) + (x₂ ∸ y₂) = (x₁ + x₂) ∸ (y₁ + y₂).
proof: Proof. intros E F. apply (right_cancellation (+) (y₁ + y₂)). rewrite cut_minus_le. setoid_replace (x₁ ∸ y₁ + (x₂ ∸ y₂) + (y₁ + y₂)) with (((x₁ ∸ y₁) + y₁) + ((x₂ ∸ y₂) + y₂)) by ring. now rewrite !cut_minus_le. now apply semirings.plus_le_compat. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax