le_gcd

Stream: new members

[Iocta]

Is there a statement similar to this?

lemma le_gcd (n r b : Int) (hr : n ∣ r) (hb : n ∣ b ) : n ≤ gcd r b := by

[Riccardo Brasca]

You can use exact? to find the statement that n divides the gcd. From there it should be immediate m

[Daniel Weber]

As stated this isn't true for r = b = 0

[suhr]

Yes:

Int.dvd_gcd {i j k : ℤ} (h1 : k ∣ i) (h2 : k ∣ j) : k ∣ ↑(i.gcd j)

You can compose it with Int.le_of_dvd {a b : ℤ} (bpos : 0 < b) (H : a ∣ b) : a ≤ b to get the function you need.