  41theorem card_vantage : Fintype.card Vantage = 3 := rfl
  42
  43/-- Every vantage has a complement pair. -/
  44def complements (v : Vantage) : Vantage × Vantage :=
  45  match v with
  46  | inside  => (act, outside)
  47  | act     => (inside, outside)
  48  | outside => (inside, act)
  49
  50/-- Cyclic successor (for the 3-phase rhythm). -/
  51def succ (v : Vantage) : Vantage :=
  52  match v with
  53  | inside  => act
  54  | act     => outside
  55  | outside => inside
  56
  57/-- Cyclic predecessor. -/
  58def pred (v : Vantage) : Vantage :=
  59  match v with
  60  | inside  => outside
  61  | act     => inside
  62  | outside => act
  63
  64theorem succ_pred_id (v : Vantage) : succ (pred v) = v := by
  65  cases v <;> rfl
  66
  67theorem pred_succ_id (v : Vantage) : pred (succ v) = v := by
  68  cases v <;> rfl
  69
  70/-- Three applications of succ returns to start. -/
  71theorem succ_succ_succ (v : Vantage) : succ (succ (succ v)) = v := by
  72  cases v <;> rfl
  73
  74end Vantage

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.