Theory MobiusGyrotrigonometry

theory MobiusGyrotrigonometry
  imports Main GammaFactor PoincareDisc MobiusGyroVectorSpace MoreComplex
begin

lemma m_gamma_h1:
  shows "⊖m a ⊕m b = of_complex ((to_complex b - to_complex a) / (1 - cnj (to_complex a) * to_complex b))"
  by (metis Mobius_gyrocarrier'.of_carrier add_uminus_conv_diff complex_cnj_minus mult_minus_left ominus_m'_def ominus_m.rep_eq oplus_m'_def oplus_m.rep_eq uminus_add_conv_diff)
  
lemma m_gamma_h2:
  shows "(⟪⊖m a ⊕m b⟫)2 = 
         ((⟪b⟫)2 + (⟪a⟫)2 - (to_complex a) * cnj (to_complex b) - cnj (to_complex a) * (to_complex b)) /
         (1 - (to_complex a) * cnj (to_complex b) - cnj(to_complex a) * (to_complex b) + (⟪a⟫)2 * (⟪b⟫)2)"
proof-
  let ?a = "to_complex a" and ?b = "to_complex b"
  have "(?b - ?a) * cnj (?b - ?a) = (⟪b⟫)2 + (⟪a⟫)2 - ?a * cnj ?b - cnj ?a * ?b"
    by (simp add: cnj_cmod mult.commute norm_p.rep_eq right_diff_distrib')
  moreover 
  have "(1 - cnj ?a * ?b) * cnj (1 - cnj ?a * ?b) =
         1 - ?a * cnj ?b - cnj ?a * ?b + (⟪a⟫)2 * (⟪b⟫)2"
    by (smt (verit, ccfv_threshold) complex_cnj_cnj complex_cnj_diff complex_cnj_mult complex_mod_cnj complex_norm_square diff_add_eq diff_diff_eq2 left_diff_distrib mult.right_neutral mult_1 norm_mult norm_p.rep_eq power_mult_distrib right_diff_distrib)
  moreover
  have "(?b - ?a) * cnj (?b - ?a) /
        ((1 - cnj ?a * ?b) * cnj (1 - cnj ?a * ?b)) =
        ⟪⊖m a ⊕m b⟫ * ⟪⊖m a ⊕m b⟫ "
    using m_gamma_h1
    by (metis (no_types, lifting) Mobius_gyrocarrier'.gyronorm_def add.commute complex_cnj_divide complex_cnj_minus complex_norm_square mult_minus_left ominus_m'_def ominus_m.rep_eq oplus_m'_def oplus_m.rep_eq power2_eq_square times_divide_times_eq uminus_add_conv_diff)
  ultimately show ?thesis
    unfolding power2_eq_square
    by metis
qed

lemma m_gamma_h3:
  shows "1 - (⟪⊖m a ⊕m b⟫)2 =
        (1 - (⟪b⟫)2 - (⟪a⟫)2 +  (⟪a⟫)2 * (⟪b⟫)2) / 
        (1 - (to_complex a) * cnj (to_complex b) - cnj (to_complex a) * (to_complex b) + (⟪a⟫)2 * (⟪b⟫)2)" (is "?lhs = ?rhs")
proof-
  let ?a = "to_complex a" and ?b = "to_complex b"
  let ?nom = "(⟪b⟫)2 + (⟪a⟫)2 - ?a * cnj ?b - cnj ?a * ?b" 
  let ?den = "1 - ?a * cnj ?b - cnj ?a * ?b + (⟪a⟫)2 * (⟪b⟫)2"

  have "?den ≠ 0"
  proof-
    have "1 - cnj ?a * ?b ≠ 0"
      by (metis complex_mod_cnj less_irrefl mult_closed_for_unit_disc norm_lt_one norm_one norm_p.rep_eq right_minus_eq)
    moreover
    have "cnj (1 - cnj ?a * ?b) ≠ 0"
      using ‹1 - cnj ?a * ?b ≠ 0›
      by fastforce
    moreover
    have "cnj (1 - cnj ?a * ?b) = 1 - ?a * cnj ?b"
      by simp
    then have "?den = (1 - cnj ?a * ?b) * cnj (1 - cnj ?a * ?b)"
      unfolding power2_eq_square
      using complex_norm_square norm_p.rep_eq
      by (simp add: left_diff_distrib power2_eq_square right_diff_distrib)
    ultimately
    show ?thesis 
      by auto
  qed

  have "?lhs = 1 - ?nom/?den"
    using m_gamma_h2
    by simp
  also have "… = (?den - ?nom) / ?den"
    using ‹?den ≠ 0›
    by (simp add: field_simps)
  also have "… = (1 - (⟪b⟫)2 - (⟪a⟫)2 + (⟪a⟫)2 * (⟪b⟫)2) / ?den"
    by force
  finally show ?thesis
    .
qed

lift_definition gammma_factor_m :: "PoincareDisc ⇒ real" ("γm") is gamma_factor
  .

lemma m_gamma_h4:
  shows "(γm (⊖m a ⊕m b))2  = 
         (1 - (to_complex a) * cnj (to_complex b) - cnj (to_complex a) * (to_complex b) + (⟪a⟫)2 * (⟪b⟫)2) / 
         (1 - (⟪b⟫)2 - (⟪a⟫)2 + (⟪a⟫)2 * (⟪b⟫)2)"
proof-
  have "(γm (⊖m a ⊕m b))2  =  1 / (1 - (⟪⊖m a ⊕m b⟫)2)"
  proof-
    have "⟪⊖m a ⊕m b⟫ < 1" 
      using norm_lt_one by auto
    then show ?thesis  
      using gamma_factor_square_norm  norm_p.rep_eq
      by (metis gammma_factor_m.rep_eq)
  qed
  then show ?thesis
    using m_gamma_h3 by auto
qed

lemma m_gamma_equation:
  shows "(γm (⊖m a ⊕m b))2 = (γm a)2 * (γm b)2 * (1 - 2 * a ⋅ b + (⟪a⟫)2 * (⟪b⟫)2)"
proof-
  let ?a = "to_complex a" and ?b = "to_complex b"
  have "2 * a ⋅ b = ?a * cnj ?b + ?b * cnj ?a"
    using Mobius_gyrocarrier'.gyroinner_def two_inner_cnj by force
  then have "1 - 2 * a ⋅b + (⟪a⟫)2 * (⟪b⟫)2 = (1 - ?a * cnj ?b - ?b * cnj ?a + (⟪a⟫)2 * (⟪b⟫)2)"
    by simp

  moreover have "(γm a)*(γm a) = 1 / (1 - (⟪a⟫)2)"
    by (metis gamma_factor_p_square_norm gammma_factor_m.rep_eq gammma_factor_p.rep_eq power2_eq_square)

  moreover have "(γm b)*(γm b) = 1 / (1 - (⟪b⟫)2)"
    by (metis gamma_factor_p_square_norm gammma_factor_m_def gammma_factor_p_def power2_eq_square)
   
  moreover have "(1 / (1 - (⟪a⟫)2)) * (1 / (1 - (⟪b⟫)2)) = 1 / (1 - (⟪a⟫)2 - (⟪b⟫)2 + (⟪a⟫)2 * (⟪b⟫)2)"
    unfolding power2_eq_square
    by (simp add: field_simps)

  ultimately show ?thesis
    using m_gamma_h4 
    unfolding power2_eq_square
    by (smt (verit, del_insts) mult.commute mult_1 of_real_1 of_real_divide of_real_eq_iff of_real_mult times_divide_eq_left)
qed

lemma T8_25_help1:
   assumes "A t ≠ B t" "A t ≠ C t" "C t ≠ B t"
           "a = (⟪Mobius_pre_gyrovector_space.get_a t⟫)2" "b = (⟪Mobius_pre_gyrovector_space.get_b t⟫)2" "c = (⟪Mobius_pre_gyrovector_space.get_c t⟫)2"
   shows "to_complex ((of_complex a) ⊕m (of_complex b) ⊕m (⊖m (of_complex c))) =
          (a + b - c - a*b*c) / (1 + a*b - a*c - b*c)" (is "?lhs = ?rhs")
proof-
  have *: "norm a < 1" "norm b < 1" "norm c < 1"
    using assms
    by (simp add: norm_geq_zero norm_lt_one power_less_one_iff)+

  have **: "1 + a*b ≠ 0"
    using abs_inner_lt_1 * by fastforce

  have "(of_complex a) ⊕m (of_complex b) = of_complex ((cor a + cor b) / (1 + cnj a * b))"
    using *
    by (metis (mono_tags, lifting) Mobius_gyrocarrier'.of_carrier Mobius_gyrocarrier'.to_carrier mem_Collect_eq norm_of_real oplus_m'_def oplus_m.rep_eq real_norm_def)

  have "?lhs = 
        (((a + b) / (1 + cnj a * b)) - c) / (1 - cnj((a + b) / (1 + cnj a * b))*c)"
    using Mobius_gyrocarrier'.to_carrier * ominus_m'_def ominus_m.rep_eq oplus_m'_def oplus_m.rep_eq real_norm_def
    by auto
  also have "... = (((a + b) / (1 + a * b)) - c) / (1 - ((a + b) / (1 + a*b)) * c)"
    by simp
  also have "… = ((a + b - c - a*b*c) / (1 + a*b)) / ((1 + a*b - a*c - b*c) / (1+a*b))"
    using **
    by (simp add: field_simps)
  also have "… = ?rhs"
    using **
    by auto
  finally show ?thesis
    .
qed

lemma T8_25_help2:
  fixes t :: "PoincareDisc otriangle"
  assumes "(A t) ≠ (B t)" "(A t) ≠ (C t)" "(C t) ≠ (B t)"
          "a = ⟪Mobius_pre_gyrovector_space.get_a t⟫" "b = ⟪Mobius_pre_gyrovector_space.get_b t⟫" "c = ⟪Mobius_pre_gyrovector_space.get_c t⟫"
          "gamma = Mobius_pre_gyrovector_space.get_gamma t"
  shows "cos gamma = (a2 + b2 - c2 - (a*b*c)2) / (2 * a * b * (1 - c2))"
proof-
  let ?a = "Mobius_pre_gyrovector_space.get_a t" and ?b = "Mobius_pre_gyrovector_space.get_b t" and ?c = "Mobius_pre_gyrovector_space.get_c t"
  have "⊖m ?a ⊕m ?b = gyrm (⊖m (C t)) (B t) ?c"
    unfolding Mobius_pre_gyrovector_space.get_a_def Mobius_pre_gyrovector_space.get_b_def Mobius_pre_gyrovector_space.get_c_def
    by (metis gyr_PoincareDisc_def gyro_translation_2a gyroinv_PoincareDisc_def gyroplus_PoincareDisc_def)
  then have "⟪⊖m ?a ⊕m ?b⟫ = ⟪?c⟫"
    by (simp add: mobius_gyroauto_norm)
  then have *: "γm (⊖m ?a ⊕m ?b) = γm ?c"
    by (simp add: gamma_factor_def gammma_factor_m.rep_eq norm_p.rep_eq)
  then have abc: "(γm (⊖m ?a ⊕m ?b))2 = (γm ?c)2"
    by presburger

  have "⊖m (C t) ⊕m A t ≠ 0m"
    using assms
    by (simp add: Mobius_gyrogroup.gyro_equation_right)
  then have "b ≠ 0" 
    using assms
    unfolding Mobius_pre_gyrovector_space.get_b_def
    using gyroinv_PoincareDisc_def gyroplus_PoincareDisc_def
    by (simp add: Mobius_gyrocarrier'.gyronorm_def)

  have "⊖m (C t) ⊕m B t ≠ 0m"
    using assms
    by (simp add: Mobius_gyrogroup.gyro_equation_right)
  then have "a ≠ 0" 
    using assms
    unfolding Mobius_pre_gyrovector_space.get_a_def
    using gyroinv_PoincareDisc_def gyroplus_PoincareDisc_def
    by (simp add: Mobius_gyrocarrier'.gyronorm_def)

  have "1 - c2 ≠ 0"
    using assms
    by (metis abs_norm_cancel dual_order.refl eq_iff_diff_eq_0 linorder_not_less norm_lt_one norm_p.rep_eq power2_eq_square real_sqrt_abs2 real_sqrt_one)

  have inner: "inner (to_complex ?a) (to_complex ?b) = a * b * cos gamma"
  proof-
    have "gamma = Mobius_pre_gyrovector_space.angle (C t) (A t) (B t)"
      using assms Mobius_pre_gyrovector_space.get_gamma_def
      by simp
    then have *: "gamma = arccos (inner (Mobius_pre_gyrovector_space.unit (⊖ (C t) ⊕ A t)) (Mobius_pre_gyrovector_space.unit (⊖ (C t) ⊕ B t)))"
      unfolding Mobius_pre_gyrovector_space.angle_def 
      by simp
    then have "cos gamma = inner (Mobius_pre_gyrovector_space.unit (⊖ (C t) ⊕ A t)) (Mobius_pre_gyrovector_space.unit (⊖ (C t) ⊕ B t))"
      using Mobius_pre_gyrovector_space.norm_inner_unit cos_arccos_abs
      by (metis real_norm_def)
    then have **: "cos gamma = (inner (Mobius_pre_gyrovector_space.unit ?a) (Mobius_pre_gyrovector_space.unit ?b))"
      using assms 
      unfolding Mobius_pre_gyrovector_space.get_a_def Mobius_pre_gyrovector_space.get_b_def
      by (simp add: inner_commute)
    
    have "cos(gamma) * a * b = inner (to_complex ?a) (to_complex (?b))"
      using ** ‹a ≠ 0› ‹b ≠ 0› assms
      unfolding Mobius_pre_gyrovector_space.unit_def
      by (metis (no_types, opaque_lifting) divide_inverse_commute inner_commute inner_scaleR_right mult.commute nonzero_mult_div_cancel_left times_divide_eq_right)
    then show ?thesis
      by (simp add: field_simps)
  qed

  have "(γm (⊖m ?a ⊕m ?b))2 = (γm ?a)2 * (γm ?b)2 * (1 - 2 * (inner (to_complex ?a) (to_complex ?b)) + (⟪?a⟫)2 * (⟪?b⟫)2)"
    using inner_p.rep_eq m_gamma_equation by presburger
  also have "… = (γm ?a)2 * (γm ?b)2 * (1 - 2 * a * b * cos(gamma) + (⟪?a⟫)2 * (⟪?b⟫)2)"
    using inner by simp
  finally have "(γm (⊖m ?a ⊕m ?b))2 / ((γm ?a)2 * (γm ?b)2) = 1 - 2 * a * b * cos(gamma) + (a2 * b2)"
    using gammma_factor_m_def gammma_factor_p_def assms by auto

  moreover

  have "(γm (⊖m ?a ⊕m ?b))2 / ((γm ?a)2 * (γm ?b)2) = ((1 - a2) * (1 - b2)) / (1 - c2)"
  proof-
    have "(γm ?a)2  = 1 / (1 - a2)" "(γm ?b)2  = 1 / (1 - b2)" "(γm ?c)2  = 1 / (1 - c2)"
      using assms
      by (metis gamma_factor_p_square_norm gammma_factor_m_def gammma_factor_p_def)+
    then show ?thesis
      using abc
      by simp
  qed

  ultimately
  have "1 - 2 * a * b * cos(gamma) + (a2 * b2) = ((1 - a2) * (1 - b2)) / (1 - c2)"
    by simp
  then show ?thesis
    using ‹a ≠ 0› ‹b ≠ 0› ‹1 - c2 ≠ 0›
    unfolding power2_eq_square
    by (simp add: field_simps)
qed   

lemma T8_25_help3:
  fixes t :: "PoincareDisc otriangle"
  assumes "(A t) ≠ (B t)" "(A t) ≠ (C t)" "(C t) ≠ (B t)"
          "a = ⟪Mobius_pre_gyrovector_space.get_a t⟫" "b = ⟪Mobius_pre_gyrovector_space.get_b t⟫" "c = ⟪Mobius_pre_gyrovector_space.get_c t⟫"
          "gamma = Mobius_pre_gyrovector_space.get_gamma t"
          "beta_a = 1 / sqrt (1 + a2)" "beta_b = 1 / sqrt (1+b2)"
        shows "2 * beta_a2 * a * beta_b2 * b * cos gamma = (a2 + b2 - c2 - (a*b*c)2) / ((1 + a2) * (1 + b2) * (1-c2))"
proof-
  have "⊖m (C t) ⊕m A t ≠ 0m"
    using assms
    by (simp add: Mobius_gyrogroup.gyro_equation_right)
  then have "b ≠ 0" 
    using assms
    unfolding Mobius_pre_gyrovector_space.get_b_def
    using gyroinv_PoincareDisc_def gyroplus_PoincareDisc_def
    by (simp add: Mobius_gyrocarrier'.gyronorm_def)
    
  have "⊖m (C t) ⊕m B t ≠ 0m"
    using assms
    by (simp add: Mobius_gyrogroup.gyro_equation_right)
  then have "a ≠ 0" 
    using assms
    unfolding Mobius_pre_gyrovector_space.get_a_def
    using gyroinv_PoincareDisc_def gyroplus_PoincareDisc_def
    by (simp add: Mobius_gyrocarrier'.gyronorm_def)

  have "1 - c2 ≠ 0"
    using assms
    by (metis abs_norm_cancel dual_order.refl eq_iff_diff_eq_0 linorder_not_less norm_lt_one norm_p.rep_eq power2_eq_square real_sqrt_abs2 real_sqrt_one)

  have "cos gamma = (a2 + b2 - c2 - (a*b*c)2) / (2 * a * b * (1 - c2))"
    using T8_25_help2 assms 
    by auto
  then have "2 * a * b * cos gamma = (a2 + b2 - c2 - (a*b*c)2) / (1 - c2)"
    using ‹a ≠ 0› ‹b ≠ 0›
    by simp
  moreover have "(beta_a2) * (beta_b2)  = 1 / ((1 + a2) * (1 + b2))"
    using assms
    by (simp_all add: power2_eq_square)
  ultimately have "2 * beta_a2 * a * beta_b2 * b * cos gamma = ((a2 + b2 - c2 - (a*b*c)2) / (1 - c2)) * 1 / ((1 + a2) * (1 + b2))"
    by (simp add: field_simps)
  then show ?thesis
    using ‹a ≠ 0› ‹b ≠ 0› ‹1 - c2 ≠ 0›
    by simp
 qed


lemma T8_25_help4:
  fixes t :: "PoincareDisc otriangle"
  assumes "(A t) ≠ (B t)" "(A t) ≠ (C t)" "(C t) ≠ (B t)"
          "a = ⟪Mobius_pre_gyrovector_space.get_a t⟫" "b = ⟪Mobius_pre_gyrovector_space.get_b t⟫" "c = ⟪Mobius_pre_gyrovector_space.get_c t⟫"
          "gamma = Mobius_pre_gyrovector_space.get_gamma t"
          "beta_a = 1 / sqrt (1 + a2)" "beta_b = 1 / sqrt (1+b2)"
    shows "1 - 2 * beta_a2 * a * beta_b2 * b * cos gamma = 
          (1 + (a*b)2 - (a*c)2 - (b*c)2) / ((1 + a2) * (1 + b2) * (1-c2))"
proof-
  have "1 + a2 ≠ 0" "1 + b2 ≠ 0"
    by (metis power_one sum_power2_eq_zero_iff zero_neq_one)+

  have "1 - c2 ≠ 0"
    using assms
    by (metis eq_iff_diff_eq_0 norm_geq_zero norm_lt_one order_less_irrefl power2_eq_square real_sqrt_abs2 real_sqrt_mult_self real_sqrt_one real_sqrt_pow2)

  have "1 - 2 * beta_a2 * a * beta_b2 * b * cos gamma = 1 - (a2 + b2 - c2 - (a*b*c)2) / ((1 + a2) * (1 + b2) * (1-c2))" (is "?lhs = 1 - ?nom / ?den")  
    using T8_25_help3 assms
    by simp
  also have "… = (?den - ?nom) / ?den"
  proof-
    have "?den ≠ 0"
      using ‹1 + a2 ≠ 0› ‹1 + b2 ≠ 0› ‹1 - c2 ≠ 0›
      by simp
    then show ?thesis
      by (simp add: field_simps)
  qed
  finally show ?thesis
    by (simp add: field_simps)
qed

lemma T25_help5:
  fixes t :: "PoincareDisc otriangle"
  assumes "(A t) ≠ (B t)" "(A t) ≠ (C t)" "(C t) ≠ (B t)"
          "a = ⟪Mobius_pre_gyrovector_space.get_a t⟫" "b = ⟪Mobius_pre_gyrovector_space.get_b t⟫" "c = ⟪Mobius_pre_gyrovector_space.get_c t⟫"
          "gamma = Mobius_pre_gyrovector_space.get_gamma t"
          "beta_a = 1 / sqrt (1 + a2)" "beta_b = 1 / sqrt (1+b2)"
    shows "(2 * beta_a2 * a * beta_b2 * b * cos gamma)  / (1 - 2 * beta_a2 * a * beta_b2 * b * cos gamma) =
           to_complex ((of_complex (a2)) ⊕m (of_complex (b2)) ⊕m (⊖m (of_complex (c2))))" (is "?lhs = ?rhs")
proof-
  let ?den = "(1+a2)*(1+b2)*(1-c2)"
  have *:"?den ≠ 0"
    using assms
    by (smt (verit, ccfv_threshold) divisors_zero norm_geq_zero norm_lt_one not_sum_power2_lt_zero pos2 power_less_one_iff)

  let ?nom1 = "a2 + b2 - c2 - (a*b*c)2" and ?nom2 = "1 + (a*b)2 - (a*c)2 - (b*c)2" 

  have "?rhs = ?nom1 / ?nom2" 
    using T8_25_help1[OF assms(1-3), of "a2" "b2" "c2"] assms
    by (simp add: power_mult_distrib)
  also have "… = (?nom1 / ?den) / (?nom2 / ?den)"
    using *
    by simp
  also have "… = (2 * beta_a2 * a * beta_b2 * b * cos gamma)  / (1 - 2 * beta_a2 * a * beta_b2 * b * cos gamma)"
    using T8_25_help3[OF assms] T8_25_help4[OF assms]
    by presburger
  finally show ?thesis
    by (simp add: cos_of_real)
qed


lemma T25_MobiusCosineLaw:
  fixes t :: "PoincareDisc otriangle"
  assumes "(A t) ≠ (B t)" "(A t) ≠ (C t)" "(C t) ≠ (B t)"
          "a = ⟪Mobius_pre_gyrovector_space.get_a t⟫" "b = ⟪Mobius_pre_gyrovector_space.get_b t⟫" "c = ⟪Mobius_pre_gyrovector_space.get_c t⟫"
          "gamma = Mobius_pre_gyrovector_space.get_gamma t"
          "beta_a = 1 / sqrt (1 + a2)" "beta_b = 1 / sqrt (1+b2)"
        shows "c2 = to_complex ((of_complex (a2)) ⊕m (of_complex (b2)) ⊕m (⊖m (of_complex 
                (2 * beta_a2 * a * beta_b2 * b * cos(gamma) /
                (1 - 2 * beta_a2 * a * beta_b2 * b * cos gamma)))))"
proof-
  let ?a = "of_complex (a2)" and ?b = "of_complex (b2)" and ?c = "of_complex (c2)"
  have "norm (c2) < 1"
     using assms
     by (simp add: norm_geq_zero norm_lt_one power_less_one_iff)+
  then have "c2 = to_complex (?a ⊕m ?b ⊕m (⊖m (?a ⊕m ?b ⊕m (⊖m ?c))))"
    using Mobius_gyrocommutative_gyrogroup.gyroautomorphic_inverse  Mobius_gyrogroup.gyrominus_def Mobius_gyrogroup.gyro_inv_idem  Mobius_gyrogroup.oplus_ominus_cancel
    by (metis (mono_tags, lifting) Mobius_gyrocarrier'.to_carrier mem_Collect_eq norm_of_real real_norm_def)
  then show ?thesis
    using T25_help5 assms
    by auto
qed

abbreviation add_complex (infixl "⊕mc" 100) where 
  "add_complex c1 c2 ≡ to_complex (of_complex c1 ⊕m of_complex c2)"

lemma T_MobiusPythagorean:
  fixes t :: "PoincareDisc otriangle"
  assumes "(A t) ≠ (B t)" "(A t) ≠ (C t)" "(C t) ≠ (B t)"
          "a = ⟪Mobius_pre_gyrovector_space.get_a t⟫" "b = ⟪Mobius_pre_gyrovector_space.get_b t⟫" "c = ⟪Mobius_pre_gyrovector_space.get_c t⟫"
          "gamma = Mobius_pre_gyrovector_space.get_gamma t" "gamma = pi / 2"
  shows "c2 = a2 ⊕mc b2"
  using assms T25_MobiusCosineLaw[OF assms(1-7)]
  by (metis (no_types, opaque_lifting) Mobius_gyrogroup.oplus_ominus_cancel cos_of_real_pi_half diff_self div_0 m_gamma_h1 mult.commute mult_zero_left of_real_divide of_real_numeral)

end