Number between integers not an integer

Stream: Is there code for X?

[Shadman Sakib]

I just proved this lemma about how a value between consecutive integers m and m+1 is not an integer. But, I'm not sure which file it should go into. Here is the proof for further details:

import analysis.complex.circle

noncomputable theory

open complex

lemma num_btw_integers_not_integer (R : Type*) [linear_ordered_ring R] (a: R) (n m: ℤ)
(h : a < m + 1) (h₀ : (m : R) < a) : a ≠ n :=
begin
  cases le_or_lt n m with n0 n1,
  { have : (n : R) ≤ m,
    { exact_mod_cast n0, },
    exact (lt_of_le_of_lt this h₀).ne', },
  { have : (m : R) + 1 ≤ n,
    { assumption_mod_cast, },
    exact (lt_of_lt_of_le h this).ne, },
end

[Shadman Sakib]

Any suggestions?

[Johan Commelin]

I would put in in the first file that imports the two files that you are importing. You can use leanproject to generate a graph of the import structure.

Minor comments:

• I would rewrite the statement as \forall n : \Z, a \ne n. In other words, put the n argument after the assumptions h and h_0. That looks more natural to me.
• I would also swap h_0 and h, I think.
• The name should be ne_int_cast_of_lt_of_lt or more verbose ne_int_cast_of_lt_int_of_int_lt or something like that.

[Mario Carneiro]

here's a simpler proof:

lemma num_btw_integers_not_integer (R : Type*) [linear_ordered_ring R] (a: R) (n m: ℤ)
(h : a < m + 1) (h₀ : (m : R) < a) : a ≠ n :=
begin
  rintro rfl,
  norm_cast at h h₀,
  exact not_le_of_lt h₀ (int.lt_add_one_iff.1 h),
end

[Yaël Dillies]

This is a special case of the typeclass succ_order I'm defining. See here #8082.

[Eric Wieser]

ne_int_cast_of_lt_of_lt_succ might be a better name. What name does your PR use?

[Kevin Buzzard]

This lemma applies to the rationals.