proof that i ≤ i+1 in Fin n

Stream: Is there code for X?

[Emily Riehl]

For i in Fin n, it should always be the case that i ≤ i+1 in the ordered set Fin (n+1) (for instance because such inequalities coincide with corresponding ones in nat). But I can't find the name for this proof. Please help!

[Ruben Van de Velde]

Is it true? For i = n-1, is i + 1 not zero?

[Yaël Dillies]

It would be true if Fin addition was saturating. (un)fortunately (depending on who you ask), it is looping around. x + y : Fin n means ⟨(x + y : ℕ) % n, Nat.mod_lt _ _⟩

[Violeta Hernández]

Does docs#Order.le_succ work?

[Violeta Hernández]

Oh oops, I missed the thing about saturating addition

[Violeta Hernández]

I think succ i should be what you want though

[Yakov Pechersky]

I think I have the relevant lemma in a PR, but in the meantime, you can use the contrapositive of docs#Fin.add_one_lt_iff

[Emily Riehl]

Ruben Van de Velde said:

Is it true? For i = n-1, is i + 1 not zero?

Thanks, I made a mistake in the statement (...though not in the code I copied the statement from). I meant to say for i in Fin n but the inequality in Fin n+1.

[Emily Riehl]

Yakov Pechersky said:

I think I have the relevant lemma in a PR, but in the meantime, you can use the contrapositive of docs#Fin.add_one_lt_iff

Thanks @Yakov Pechersky. Will you ping me once it's merged?

[Yaël Dillies]

Your statement should then be ∀ i : Fin n, i.castSucc ≤ i.succ, which you can prove using docs#Fin.castSucc_lt_succ_iff and docs#le_rfl

[Emily Riehl]

Thanks! In parallel, I discovered that this also works for me:

theorem Fin.le_succ {n} (i : Fin n) : i.castSucc ≤ i.succ := Nat.le_succ i

def Fin.hom_succ {n} (i : Fin n) : i.castSucc ⟶ i.succ := homOfLE (Fin.le_succ i)