tenfold_squared

formal source

  65  rw [hA, hB]
  66
  67/-- 10 × 10 = 100. -/
  68theorem tenfold_squared
  69    {A B : Type} [Fintype A] [Fintype B]
  70    (hA : HasTenFold A) (hB : HasTenFold B) :
  71    Fintype.card (A × B) = 100 := by
  72  unfold HasTenFold at hA hB
  73  simp [Fintype.card_prod, hA, hB]
  74
  75/-- 10 × D = 50. 50 is still below gap45+5. -/
  76theorem tenfold_times_D : (10 : ℕ) * 5 = 50 := by decide
  77
  78/-- Two 5-fold halves of a 10-fold: decimal = 2 × 5 (half-halves). -/
  79theorem ten_as_two_halves : (10 : ℕ) = 5 + 5 := by decide
  80
  81structure TenFoldCombinationsCert where
  82  finger_10 : HasTenFold Finger
  83  digit_10 : HasTenFold DecimalDigit
  84  lumSac_10 : HasTenFold LumbarSacralVert
  85  dBlock_10 : HasTenFold DBlockElement
  86  ten_factoring : (10 : ℕ) = 2 * 5
  87  ten_as_halves : (10 : ℕ) = 5 + 5
  88  squared_100 : ∀ (A B : Type) [Fintype A] [Fintype B],
  89    HasTenFold A → HasTenFold B → Fintype.card (A × B) = 100
  90
  91def tenFoldCombinationsCert : TenFoldCombinationsCert where
  92  finger_10 := finger_is_10
  93  digit_10 := digit_is_10
  94  lumSac_10 := lumSac_is_10
  95  dBlock_10 := dBlock_is_10
  96  ten_factoring := ten_eq_two_D
  97  ten_as_halves := ten_as_two_halves
  98  squared_100 := fun _ _ _ _ => tenfold_squared