Streamline proofs

[clayrat]

Inequalities:

• Have a set of inductive inequality definitions (http://www.reddit.com/r/Idris/comments/6ya7jg/unification_problems_associated_with_totality/), and bijections to the witness-style ones currently used?
• Reduce code duplication for ltGt, leTrans and others: interfaces, elaborator macros?
• Fix order of arguments in Bin and Biz versions of addCompareMonoR

[clayrat]

• Use sections more, e.g. (bizMult 2) -> (2*) (esp now that https://github.com/idris-lang/Idris-dev/pull/4119 is merged)
• Look for places where two rewrites/replaces can be rolled into trans

[clayrat]

Order of multiplication in the divMod-style proofs: in some places it's b*q+r, in others it's q*b+r; would be nice to choose a single style (personally I like q*b+r more) to avoid extra mulComms.

[clayrat]

Introduce lemmas to do rewrites like a 'compare' (b+c) = (a-c) 'compare' b directly, without addAssoc and posSubDiag

[clayrat]

Try to simplify *Spec types by removing explicit equalities ala:

%default total

data NatM = NatO | NatP Nat | NatN

data NatMSpec : (p, q : Nat) -> (m : NatM) -> Type where
  SubIsNul :              NatMSpec p p NatO
  SubIsPos : q + r = p -> NatMSpec p q (NatP r)
  SubIsNeg : p + r = q -> NatMSpec p q NatN

minusM : Nat -> Nat -> NatM
minusM Z        Z         = NatO
minusM Z        (S _)     = NatN
minusM left     Z         = NatP left
minusM (S left) (S right) = minusM left right

minusSpec_step : NatMSpec p q s -> NatMSpec (S p) (S q) s
minusSpec_step SubIsNul = SubIsNul
minusSpec_step (SubIsPos eq) = SubIsPos (cong eq)
minusSpec_step (SubIsNeg eq) = SubIsNeg (cong eq)

minusSpec : (p, q : Nat) -> NatMSpec p q (minusM p q)
minusSpec Z Z = SubIsNul
minusSpec Z (S k) = SubIsNeg {r=S k} Refl
minusSpec (S k) Z = SubIsPos Refl
minusSpec (S k) (S j) = minusSpec_step (minusSpec k j)

or even

SubIsPos : NatMSpec (q + r) q (NatP r)

[clayrat]

Try wrapping signed (and unsigned?) in records to prevent over-normalization a-la Box in https://gallais.github.io/pdf/agdarsec17.pdf