beats

formal source

  25
  26namespace Beat
  27
  28@[simp] def beats : Nat := Nat.lcm 8 45
  29
  30@[simp] lemma beats_eq_360 : beats = 360 := by
  31  simp [beats, lcm_8_45_eq_360]
  32
  33@[simp] lemma cycles_of_8 : beats / 8 = 45 := by
  34  simp [beats, lcm_8_45_div_8]
  35
  36@[simp] lemma cycles_of_45 : beats / 45 = 8 := by
  37  simp [beats, lcm_8_45_div_45]
  38
  39lemma minimal_sync_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : beats ∣ t := by
  40  simpa [beats] using Nat.lcm_dvd h8 h45
  41
  42lemma minimal_sync_360_divides {t : Nat} (h8 : 8 ∣ t) (h45 : 45 ∣ t) : 360 ∣ t := by
  43  simpa [beats_eq_360] using minimal_sync_divides (t:=t) h8 h45
  44
  45lemma no_smaller_multiple_8_45 {n : Nat} (hnpos : 0 < n) (hnlt : n < 360) :
  46  ¬ (8 ∣ n ∧ 45 ∣ n) := by
  47  intro h; rcases h with ⟨h8, h45⟩
  48  have h360 : 360 ∣ n := minimal_sync_360_divides (t:=n) h8 h45
  49  rcases h360 with ⟨k, hk⟩
  50  rcases Nat.eq_zero_or_pos k with rfl | hkpos
  51  · -- k = 0, so n = 360 * 0 = 0, contradicting hnpos : 0 < n
  52    simp only [Nat.mul_zero] at hk
  53    omega
  54  · have : 360 ≤ 360 * k := Nat.mul_le_mul_left 360 hkpos
  55    have : 360 ≤ n := by simpa [hk] using this
  56    exact (not_le_of_gt hnlt) this
  57
  58structure Sync where