(b + c) % d < a → b + c < a

Stream: new members

[Tobias Grosser]

(deleted)

[Tobias Grosser]

(deleted)

[Tobias Grosser]

(deleted)

[Tobias Grosser]

(deleted)

[Notification Bot]

Tobias Grosser has marked this topic as resolved.

[Tobias Grosser]

Let me think about this further. This is not even true.

[Yaël Dillies]

Are you looking for docs#Nat.mod_eq_of_lt ?

[Tobias Grosser]

No, I am trying to proof:

2 ^ w ≤ b + c
⊢ (b + c) % 2 ^ w < a → b + c < a

[Tobias Grosser]

And am looking for the right lemma.

[Notification Bot]

Tobias Grosser has marked this topic as unresolved.

[Yaël Dillies]

Yeah indeed you're going to need more assumptions

[Tobias Grosser]

Should this lemma not hold?

def should_this_hold {a b c : Nat} (h : c ≤ b) : b % c < a → b < a := by
  sorry

[Tobias Grosser]

My proof goes through if this lemma would hold

[Yaël Dillies]

Take a = 2, b = 3, c = 2

[Tobias Grosser]

OK. I need to switch topics.

[Tobias Grosser]

I had hoped I can bash this somehow. Need to think about this more carefully. Thank you.