Library ssrnat_ext

Require Import ssreflect ssrbool ssrnat.
Export ssrnat.

Lemma leq_and_ltn' : forall l l', l <= l' < l = false.

Lemma leq_and_ltn'' : forall l l', l <= l' < l.+1 -> l = l'.

Lemma ltn_total : forall l l', l < l' \/ l' <= l.

Lemma ltn_leq_trans : forall n m p, m < n -> n <= p -> m < p.

Lemma eq_succ : forall l, ~ l = l.+1.

Ltac arith_hypo_ssrnat2coqnat :=
  match goal with
    | H : context [?L < ?R] |- _ => move/ltP: H => H
    | H : context [?L <= ?R] |- _ => move/leP: H => H
    | H : context [?L < ?M < ?R] |- _ => let H1 := fresh in case/andP: H => H H1
    | H : context [?L <= ?M < ?R] |- _ => let H1 := fresh in case/andP: H => H H1
  end.


Ltac arith_goal_ssrnat2coqnat :=
  rewrite -?plusE ;
  match goal with
    | |- is_true (_ < _)%nat => apply/ltP
    | |- _ => idtac
  end.

Require Import Omega.

Ltac ssrnat_omega :=
  repeat arith_hypo_ssrnat2coqnat ;
  arith_goal_ssrnat2coqnat ;
  omega.