Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]

Require Import Lia.

(* Adopted from http://github.com/pi8027/formalized-postscript/blob/master/stdlib_ext.v *)

(** This tactic matches over the hypotheses, searching for expressions that can 
      be converted from [ssreflect] arithmetic to Coq arithmetic. *) 
Ltac arith_hypo_ssrnat2coqnat :=
  match goal with
  | H : context [andb _ _] |- _ => let H0 := fresh in case/andP: H => H H0
  | H : context [orb _ _] |- _ => case/orP: H => H
  | H : context [?L <= ?R] |- _ => move/leP: H => H
  | H : context [?L < ?R] |- _ => move/ltP : H => H
  | H : context [?L == ?R] |- _ => move/eqP : H => H
  | H : context [addn ?L ?R] |- _ => rewrite -plusE in H
  | H : context [muln ?L ?R] |- _ => rewrite -multE in H
  | H : context [subn ?L ?R] |- _ => rewrite -minusE in H
  end.

(** This tactic matches the goal, searching for expressions that can be 
      converted from [ssreflect] arithmetic to Coq arithmetic. *) 
Ltac arith_goal_ssrnat2coqnat :=
  rewrite ?NatTrec.trecE -?plusE -?minusE -?multE -?leqNgt -?ltnNge;
  repeat match goal with
         | |- is_true (andb _ _) => apply/andP; split
         | |- is_true (orb _ _) => try apply/orP
         | |- is_true (_ <= _) => try apply/leP
         | |- is_true (_ < _) => try apply/ltP
         end.

(** Solves linear integer arithmetic goals containing [ssreflect] expressions. 
    This tactic first rewrites the context to replace operations from [ssreflect]
    to the corresponding operations in the Coq library, then calls [lia]. *)
Ltac ssrlia :=
  repeat arith_hypo_ssrnat2coqnat; arith_goal_ssrnat2coqnat;
  simpl;
  lia.