to_nat_le_to_nat (#685)

Author: sgouezel

src/data/int/basic.lean

@@ -718,6 +718,9 @@ by rw [to_nat_eq_max]; apply le_max_left
 by rw [(coe_nat_le_coe_nat_iff _ _).symm, to_nat_eq_max, max_le_iff];
    exact and_iff_left (coe_zero_le _)
 
+theorem to_nat_le_to_nat {a b : ℤ} (h : a ≤ b) : to_nat a ≤ to_nat b :=
+by rw to_nat_le; exact le_trans h (le_to_nat b)
+
 def to_nat' : ℤ → option ℕ
 | (n : ℕ) := some n
 | -[1+ n] := none