c ∈ set.Icc a b → (d * c) ∈ set.Icc (d * a) (d * b)

Stream: Is there code for X?

[Violeta Hernández]

Do we have this already?

[Violeta Hernández]

It's a very simple lemma to prove, but I think it would still be nice to have

[Yaël Dillies]

The real interesting lemma is d • Icc a = Icc (d • a) (d • b).

[Yaël Dillies]

If you use intervals, it's not to talk about their membership, because you should simp it away.

[Violeta Hernández]

Ah, I see.

[Violeta Hernández]

Well, if that's the convention, then I won't be needing this lemma.