resolves issue #1800: deprecates ≤-step etc. throughout

[jamesmckinna]

Additionally,

• [x] some dependencies lightened (in favour of other lemmas from Data.Nat.Properties)
• [x] made corresponding changes to <-step as m<n⇒m<1+n
• [x] added pattern synonym m≤′n⇒m≤′1+n for ≤′-step by analogy
• [x] renamed pattern synonym <′-base to n<′1+n; corresponding knock-on changes to Data.Nat.Properties
• [x] renamed pattern synonym <′-step to m<′n⇒m<′1+n; corresponding knock-on changes to Data.Nat.{Properties|Induction}
• [x] Data.Integer.Properties
• [x] Data.Rational.Unnormalised.Properties
• [x] Data.Rational.Properties (actually nothing to change here)

UPDATED: done

[jamesmckinna]

OK, good to go now, I think.