my arch-nemesis atm

mod-arith.lean

import Batteries


def NModB251CC8 := Vector (Fin 251) 4
def MAX_VAL := (250 * 251^0) + (250 * 251^1) + (250 * (251 ^ 2)) + (250 * (251 ^ 3))
def NModSC := Fin (MAX_VAL + 1)

def from_NModB251CC8_to_Nat : NModB251CC8 -> Nat | i => (i.zipWithIndex.map (fun ⟨ a , i ⟩ => a * ((251:Nat) ^ i))).foldl Nat.add 0

example : from_NModB251CC8_to_Nat (Vector.mk #[250,250,250,250] (by decide)) < MAX_VAL + 1 := by trivial

def upper_limit_ind_pr : 
  (from_NModB251CC8_to_Nat (Vector.mk #[250-a,250-b,250-c,250-c] (by rfl)) < MAX_VAL + 1) 
  -> from_NModB251CC8_to_Nat k < MAX_VAL + 1 
:= by
  admit



def upper_limit : ∀ k, from_NModB251CC8_to_Nat k < MAX_VAL + 1 := by
  intro i
  admit
--   unfold MAX_VAL
--   simp
--   let ⟨ items , size ⟩ := i
--   induction items
--   case _ p =>
--   simp at size
--   let (.cons c1 (.cons c2 (.cons c3 (.cons c4 .nil)))) := p
--   induction c1

--   admit
  

def from_NModB251CC8_to_NModSC : NModB251CC8 -> NModSC 
| i => by 
  let indexed := from_NModB251CC8_to_Nat i
  refine Fin.mk indexed ?_
  apply upper_limit