minimal_sync_divides

formal source

  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
  59  beats : Nat
  60  cycles8 : beats / 8 = 45
  61  cycles45 : beats / 45 = 8
  62
  63noncomputable def canonical : Sync :=
  64  { beats := beats
  65  , cycles8 := cycles_of_8
  66  , cycles45 := cycles_of_45 }
  67
  68end Beat
  69