proposition: Lemma cut_minus_plus_toggle3 x₁ x₂ y₁ y₂ : x₁ ≤ y₁ → y₂ ≤ x₂ → (y₁ ∸ x₁) + ((x₁ + x₂) ∸ (y₁ + y₂)) = (x₂ ∸ y₂) + ((y₁ + y₂) ∸ (x₁ + x₂)).
proof: Proof. intros. destruct (total (≤) (x₁ + x₂) (y₁ + y₂)). rewrite (cut_minus_0 (x₁ + x₂) (y₁ + y₂)) by easy. rewrite cut_minus_plus_distr by easy. setoid_replace (x₂ + (y₁ + y₂)) with (y₁ + (x₂ + y₂)) by ring. setoid_replace (y₂ + (x₁ + x₂)) with (x₁ + (x₂ + y₂)) by ring. rewrite <-cut_minus_plus_rev_r. ring. rewrite (cut_minus_0 (y₁ + y₂) (x₁ + x₂)) by easy. rewrite cut_minus_plus_distr by easy. setoid_replace (y₁ + (x₁ + x₂)) with (x₂ + (x₁ + y₁)) by ring. setoid_replace (x₁ + (y₁ + y₂)) with (y₂ + (x₁ + y₁)) by ring. rewrite <-cut_minus_plus_rev_r. ring. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.orders.minmax