feat(analysis/special_functions/trigonometric/angle): more on angles …

…equal or not equal to 0 or π (#16055)

We have various lemmas giving conditions for an angle to equal 0 or π.
Add some more such lemmas, plus negated versions of existing lemmas
giving conditions for angles not to equal 0 or π.

src/analysis/special_functions/trigonometric/angle.lean

@@ -105,9 +105,27 @@ by simp_rw [←coe_nat_zsmul, int.coe_nat_bit0, int.coe_nat_one, two_zsmul_eq_if
 lemma two_nsmul_eq_zero_iff {θ : angle} : (2 : ℕ) • θ = 0 ↔ (θ = 0 ∨ θ = π) :=
 by convert two_nsmul_eq_iff; simp
 
+lemma two_nsmul_ne_zero_iff {θ : angle} : (2 : ℕ) • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ π :=
+by rw [←not_or_distrib, ←two_nsmul_eq_zero_iff]
+
 lemma two_zsmul_eq_zero_iff {θ : angle} : (2 : ℤ) • θ = 0 ↔ (θ = 0 ∨ θ = π) :=
 by simp_rw [two_zsmul, ←two_nsmul, two_nsmul_eq_zero_iff]
 
+lemma two_zsmul_ne_zero_iff {θ : angle} : (2 : ℤ) • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ π :=
+by rw [←not_or_distrib, ←two_zsmul_eq_zero_iff]
+
+lemma eq_neg_self_iff {θ : angle} : θ = -θ ↔ θ = 0 ∨ θ = π :=
+by rw [←add_eq_zero_iff_eq_neg, ←two_nsmul, two_nsmul_eq_zero_iff]
+
+lemma ne_neg_self_iff {θ : angle} : θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ π :=
+by rw [←not_or_distrib, ←eq_neg_self_iff.not]
+
+lemma neg_eq_self_iff {θ : angle} : -θ = θ ↔ θ = 0 ∨ θ = π :=
+by rw [eq_comm, eq_neg_self_iff]
+
+lemma neg_ne_self_iff {θ : angle} : -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ π :=
+by rw [←not_or_distrib, ←neg_eq_self_iff.not]
+
 theorem cos_eq_iff_coe_eq_or_eq_neg {θ ψ : ℝ} :
   cos θ = cos ψ ↔ (θ : angle) = ψ ∨ (θ : angle) = -ψ :=
 begin
@@ -227,6 +245,9 @@ begin
   simp
 end
 
+lemma sin_ne_zero_iff {θ : angle} : sin θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ π :=
+by rw [←not_or_distrib, ←sin_eq_zero_iff]
+
 @[simp] lemma sin_neg (θ : angle) : sin (-θ) = -sin θ :=
 begin
   induction θ using real.angle.induction_on,
@@ -303,6 +324,9 @@ by simp [sign_antiperiodic.sub_eq']
 lemma sign_eq_zero_iff {θ : angle} : θ.sign = 0 ↔ θ = 0 ∨ θ = π :=
 by rw [sign, sign_eq_zero_iff, sin_eq_zero_iff]
 
+lemma sign_ne_zero_iff {θ : angle} : θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ π :=
+by rw [←not_or_distrib, ←sign_eq_zero_iff]
+
 end angle
 
 end real