diff --git a/.github/workflows/deploy-docs.yml b/.github/workflows/deploy-docs.yml
deleted file mode 100644
index c5243c3..0000000
--- a/.github/workflows/deploy-docs.yml
+++ /dev/null
@@ -1,59 +0,0 @@
-name: Build and Deploy documentation
-
-on:
-  push:
-    branches:
-      - master
-  pull_request:
-    branches:
-      - '**'
-
-jobs:
-  build-coqdoc:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Set up Git repository
-        uses: actions/checkout@v2
-
-      - name: Build coqdoc
-        uses: coq-community/docker-coq-action@v1
-        with:
-          custom_image: 'coqorg/coq:dev'
-          custom_script: |
-            {{before_install}}
-            startGroup "Build aac-tactics dependencies"
-              opam pin add -n -y -k path coq-aac-tactics .
-              opam update -y
-              opam install -y -j "$(nproc)" coq-aac-tactics --deps-only
-            endGroup
-            startGroup "Add permissions"
-              sudo chown -R coq:coq .
-            endGroup
-            startGroup "Build aac-tactics"
-              make -j "$(nproc)"
-            endGroup
-            startGroup "Build coqdoc"
-              make coqdoc
-            endGroup
-            startGroup "Build ocamldoc"
-              make ocamldoc
-            endGroup
-
-      - name: Revert Coq user permissions
-        # to avoid a warning at cleanup time
-        if: ${{ always() }}
-        run: sudo chown -R 1001:116 .
-
-      - name: Copy HTML and CSS and JavaScript
-        run: |
-          mkdir public
-          cp -r resources/index.html docs/ public/
-
-      - name: Deploy to GitHub pages
-        if: github.event_name == 'push' && github.ref == 'refs/heads/master'
-        uses: crazy-max/ghaction-github-pages@v2
-        with:
-          build_dir: public
-          jekyll: false
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/.gitignore b/.gitignore
index 52070c8..9064803 100644
--- a/.gitignore
+++ b/.gitignore
@@ -20,6 +20,7 @@
 
 src/aac.ml
 .lia.cache
+.nia.cache
 .merlin
 Makefile.coq
 Makefile.coq.conf
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..9e2bd80
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,20 @@
+# Changelog
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
+
+## [Unreleased]
+
+## [8.19.1] - 2024-06-01
+
+### Added
+
+- `aac_normalise in H` tactic.
+- `gcd` and `lcm` instances for `Nat`, `N`, and `Z`.
+
+### Fixed
+
+- Make the order of sums produced by `aac_normalise` tactic consistent across calls.
+
+[Unreleased]: https://github.com/coq-community/chapar/compare/v8.19.1...master
+[8.19.1]: https://github.com/coq-community/chapar/releases/tag/v8.19.1
diff --git a/src/matcher.ml b/src/matcher.ml
index 787e02e..2e154f9 100644
--- a/src/matcher.ml
+++ b/src/matcher.ml
@@ -108,6 +108,9 @@ module Terms : sig
   val equal_aac : units -> t -> t -> bool
   val size: t -> int
 
+  (* permute symbols according to p *)
+  val map_syms: (symbol -> symbol) -> t -> t
+
   (** {1 Terms in normal form}
      
       A term in normal form is the canonical representative of the
@@ -162,6 +165,13 @@ end
       | Sym (_,v)-> Array.fold_left (fun acc x -> size x + acc) 1 v
       | _ -> 1
 
+    (* permute symbols according to p *)
+    let rec map_syms p = function
+      | Dot(s,u,v) -> Dot(p s, map_syms p u, map_syms p v)
+      | Plus(s,u,v) -> Plus(p s, map_syms p u, map_syms p v)
+      | Sym(s,u) -> Sym(p s, Array.map (map_syms p) u)
+      | Unit s -> Unit(p s)
+      | u -> u
 
     type nf_term =
       | TAC of  symbol * nf_term mset
diff --git a/src/matcher.mli b/src/matcher.mli
index a6b6f46..0894528 100644
--- a/src/matcher.mli
+++ b/src/matcher.mli
@@ -118,6 +118,8 @@ sig
       units of a same operator are not considered equal.  *)
   val equal_aac : units ->  t -> t -> bool
 
+  (* permute symbols according to p *)
+  val map_syms: (symbol -> symbol) -> t -> t
 
   (** {2 Normalised terms (canonical representation) }
      
diff --git a/src/theory.ml b/src/theory.ml
index aaa9864..e4a7705 100644
--- a/src/theory.ml
+++ b/src/theory.ml
@@ -724,6 +724,24 @@ module Trans = struct
     let sigma = Gather.gather env sigma rlt envs (EConstr.of_constr (Constr.mkApp (l, [| Constr.mkRel 0;Constr.mkRel 0|]))) in
     sigma
 
+  (* reorder the environment to make it (more) canonical *)
+  let reorder envs =
+    let rec insert k v = function
+      | [] -> [k,v]
+      | ((h,_)::_) as l when Constr.compare k h = -1 -> (k,v)::l
+      | y::q -> y::insert k v q
+    in
+    let insert k v l =
+      match v with Some v -> insert k v l | None -> l
+    in
+    let l = HMap.fold insert envs.discr [] in
+    let old = Hashtbl.copy envs.bloom_back in
+    PackTable.clear envs.bloom;
+    Hashtbl.clear envs.bloom_back;
+    envs.bloom_next := 1;
+    List.iter (fun (c,pack) -> add_bloom envs pack) l;
+    (fun s -> PackTable.find envs.bloom (Hashtbl.find old s))
+  
   (* [t_of_constr] buils a the abstract syntax tree of a constr,
      updating in place the environment. Doing so, we infer all the
      morphisms and the AC/A operators. It is mandatory to do so both
@@ -734,7 +752,8 @@ module Trans = struct
     let sigma = Gather.gather env sigma rlt envs r in
     let l,sigma = Parse.t_of_constr env sigma rlt envs l in
     let r, sigma = Parse.t_of_constr env sigma rlt envs r in
-    l, r, sigma
+    let p = reorder envs in
+    Matcher.Terms.map_syms p l, Matcher.Terms.map_syms p r, sigma
 
   (* An intermediate representation of the environment, with association lists for AC/A operators, and also the raw [packer] information *)
 
@@ -967,25 +986,6 @@ module Trans = struct
     in
       sigma,record
 
-  (* We want to lift down the indexes of symbols. *)
-  let renumber (l: (int * 'a) list ) =
-    let _, l = List.fold_left (fun (next,acc) (glob,x) ->
-				 (next+1, (next,glob,x)::acc)
-			      ) (1,[]) l
-    in
-    let rec to_global loc = function
-      | [] -> assert false
-      | (local, global,x)::q when  local = loc -> global
-      | _::q -> to_global loc q
-    in
-    let rec to_local glob = function
-      | [] -> assert false
-      | (local, global,x)::q when  global = glob -> local
-      | _::q -> to_local glob q
-    in
-    let locals = List.map (fun (local,global,x) -> local,x) l in
-      locals, (fun x -> to_local x l) , (fun x -> to_global x l)
-
   (** [build_sigma_maps] given a envs and some reif_params, we are
       able to build the sigmas *)
   let build_sigma_maps (rlt : Coq.Relation.t) zero ir : (sigmas * sigma_maps) Proofview.tactic =
@@ -996,11 +996,10 @@ module Trans = struct
         let env = Proofview.Goal.env goal in
         let sigma,rp = build_reif_params env sigma rlt zero in
         Unsafe.tclEVARS sigma
-        <*> let renumbered_sym, to_local, to_global = renumber ir.sym  in
-            let env_sym = Sigma.of_list
+        <*> let env_sym = Sigma.of_list
                             rp.sym_ty
                             (rp.sym_null)
-                            renumbered_sym
+                            ir.sym
             in 
             Coq.mk_letin "env_sym" env_sym >>= fun env_sym ->
             let bin = (List.map ( fun (n,s) -> n, Bin.mk_pack rlt s) ir.bin) in
@@ -1029,8 +1028,8 @@ module Trans = struct
             let f = List.map (fun (x,_) -> (x,Coq.Pos.of_int x)) in
             let sigma_maps =
               {
-	        sym_to_pos = (let sym = f renumbered_sym in fun x ->  (List.assoc (to_local x) sym));
-	        bin_to_pos = (let bin = f bin in fun x ->  (List.assoc  x bin));
+	        sym_to_pos = (let sym = f ir.sym in fun x ->  (List.assoc x sym));
+	        bin_to_pos = (let bin = f bin in fun x ->  (List.assoc x bin));
 	        units_to_pos = (let units = f units in fun x ->  (List.assoc  x units));
               }
             in
diff --git a/theories/AAC.v b/theories/AAC.v
index 7298663..febd1e5 100644
--- a/theories/AAC.v
+++ b/theories/AAC.v
@@ -281,14 +281,14 @@ Section s.
   (** Lexicographic rpo over the normalised syntax *)
   Fixpoint compare (u v: T) :=
     match u,v with
-      | sum i l, sum j vs => lex (idx_compare i j) (mset_compare compare l vs)
-      | prd i l, prd j vs => lex (idx_compare i j) (list_compare compare l vs)
-      | sym i l, sym j vs => lex (idx_compare i j) (vcompare l vs)
-      | unit i , unit j => idx_compare i j
+      | sum i l, sum j vs => lex (Pos.compare i j) (mset_compare compare l vs)
+      | prd i l, prd j vs => lex (Pos.compare i j) (list_compare compare l vs)
+      | sym i l, sym j vs => lex (Pos.compare i j) (vcompare l vs)
+      | unit i , unit j => Pos.compare i j
       | unit _ , _        => Lt
-      | _      , unit _  => Gt
-      | sum _ _, _        => Lt
-      | _      , sum _ _  => Gt
+      | _      , unit _   => Gt
+      | sym _ _,  _       => Lt
+      | _      , sym _ _  => Gt
       | prd _ _, _        => Lt
       | _      , prd _ _  => Gt
 
@@ -335,14 +335,14 @@ Section s.
       case (pos_compare_weak_spec p p0); intros; try constructor.
       case (list_compare_weak_spec compare tcompare_weak_spec n n0); intros; try constructor.
     - destruct v0; simpl; try constructor.
-      case_eq (idx_compare i i0); intro Hi; try constructor.
+      case_eq (Pos.compare i i0); intro Hi; try constructor.
       (* the [symmetry] is required *)
-      apply idx_compare_reflect_eq in Hi. symmetry in Hi. subst.       
+      apply pos_compare_reflect_eq in Hi. symmetry in Hi. subst.
       case_eq (vcompare v v0); intro Hv; try constructor.
       rewrite <- (vcompare_reflect_eqdep _ _ _ _ eq_refl Hv). constructor.
     - destruct v; simpl; try constructor.
-      case_eq (idx_compare p p0); intro Hi; try constructor.
-      apply idx_compare_reflect_eq in Hi. symmetry in Hi. subst.  constructor.
+      case_eq (Pos.compare p p0); intro Hi; try constructor.
+      apply pos_compare_reflect_eq in Hi. symmetry in Hi. subst.  constructor.
     - induction us; destruct vs; simpl; intros H Huv; try discriminate.
       apply cast_eq, eq_nat_dec.
       injection H; intro Hn.
@@ -961,3 +961,15 @@ Section t.
 End t.
        
 Declare ML Module "aac_plugin:coq-aac-tactics.plugin".
+
+Lemma transitivity4 {A R} {H: @Equivalence A R} a b a' b': R a a' -> R b b' -> R a b -> R a' b'.
+Proof. now intros -> ->. Qed.
+Tactic Notation "aac_normalise" "in" hyp(H) :=
+  eapply transitivity4 in H; [| aac_normalise; reflexivity | aac_normalise; reflexivity].
+
+Ltac aac_normalise_all :=
+    aac_normalise;
+    repeat match goal with
+      | H: _ |- _ => aac_normalise in H
+      end.
+Tactic Notation "aac_normalise" "in" "*" := aac_normalise_all.
diff --git a/theories/Instances.v b/theories/Instances.v
index 87b3c9c..b199351 100644
--- a/theories/Instances.v
+++ b/theories/Instances.v
@@ -34,13 +34,25 @@ Module Peano.
   #[export] Instance aac_Nat_max_Comm : Commutative eq Nat.max := Nat.max_comm.
   #[export] Instance aac_Nat_max_Assoc : Associative eq Nat.max := Nat.max_assoc.
   #[export] Instance aac_Nat_max_Idem : Idempotent eq Nat.max := Nat.max_idempotent.
- 
+
+  #[export] Instance aac_Nat_gcd_Comm : Commutative eq Nat.gcd := Nat.gcd_comm.
+  #[export] Instance aac_Nat_gcd_Assoc : Associative eq Nat.gcd := Nat.gcd_assoc.
+  #[export] Instance aac_Nat_gcd_Idem : Idempotent eq Nat.gcd := Nat.gcd_diag.
+
+  #[export] Instance aac_Nat_lcm_Comm : Commutative eq Nat.lcm := Nat.lcm_comm.
+  #[export] Instance aac_Nat_lcm_Assoc : Associative eq Nat.lcm := Nat.lcm_assoc.
+  #[export] Instance aac_Nat_lcm_Idem : Idempotent eq Nat.lcm := Nat.lcm_diag.
+
   #[export] Instance aac_Nat_mul_1_Unit : Unit eq Nat.mul 1 :=
     Build_Unit eq Nat.mul 1 Nat.mul_1_l Nat.mul_1_r.
+  #[export] Instance aac_Nat_lcm_1_Unit : Unit eq Nat.lcm 1 :=
+    Build_Unit eq Nat.lcm 1 Nat.lcm_1_l Nat.lcm_1_r.
   #[export] Instance aac_Nat_add_0_Unit : Unit eq Nat.add 0 :=
     Build_Unit eq Nat.add (0) Nat.add_0_l Nat.add_0_r.
   #[export] Instance aac_Nat_max_0_Unit : Unit eq Nat.max 0 :=
     Build_Unit eq Nat.max 0 Nat.max_0_l Nat.max_0_r.
+  #[export] Instance aac_Nat_gcd_0_Unit : Unit eq Nat.gcd 0 :=
+    Build_Unit eq Nat.gcd 0 Nat.gcd_0_l Nat.gcd_0_r.
 
   (** We also provide liftings from  [Nat.le] to [eq] *)
   #[export] Instance Nat_le_PreOrder : PreOrder Nat.le :=
@@ -68,7 +80,13 @@ Module Z.
   #[export] Instance aac_Z_max_Comm : Commutative eq Z.max := Z.max_comm.
   #[export] Instance aac_Z_max_Assoc : Associative eq Z.max := Z.max_assoc.
   #[export] Instance aac_Z_max_Idem : Idempotent eq Z.max := Z.max_idempotent.
- 
+
+  #[export] Instance aac_Z_gcd_Comm : Commutative eq Z.gcd := Z.gcd_comm.
+  #[export] Instance aac_Z_gcd_Assoc : Associative eq Z.gcd := Z.gcd_assoc.
+
+  #[export] Instance aac_Z_lcm_Comm : Commutative eq Z.lcm := Z.lcm_comm.
+  #[export] Instance aac_Z_lcm_Assoc : Associative eq Z.lcm := Z.lcm_assoc.
+  
   #[export] Instance aac_Z_mul_1_Unit : Unit eq Z.mul 1 :=
     Build_Unit eq Z.mul 1 Z.mul_1_l Z.mul_1_r.
   #[export] Instance aac_Z_add_0_Unit : Unit eq Z.add 0 :=
@@ -123,13 +141,25 @@ Module N.
   #[export] Instance aac_N_max_Comm : Commutative eq N.max := N.max_comm.
   #[export] Instance aac_N_max_Assoc : Associative eq N.max := N.max_assoc.
   #[export] Instance aac_N_max_Idem : Idempotent eq N.max := N.max_idempotent.
+  
+  #[export] Instance aac_N_gcd_Comm : Commutative eq N.gcd := N.gcd_comm.
+  #[export] Instance aac_N_gcd_Assoc : Associative eq N.gcd := N.gcd_assoc.
+  #[export] Instance aac_N_gcd_Idem : Idempotent eq N.gcd := N.gcd_diag.
+
+  #[export] Instance aac_N_lcm_Comm : Commutative eq N.lcm := N.lcm_comm.
+  #[export] Instance aac_N_lcm_Assoc : Associative eq N.lcm := N.lcm_assoc.
+  #[export] Instance aac_N_lcm_Idem : Idempotent eq N.lcm := N.lcm_diag.
 
   #[export] Instance aac_N_mul_1_Unit : Unit eq N.mul (1)%N :=
-    Build_Unit eq N.mul (1)%N N.mul_1_l N.mul_1_r.
+    Build_Unit eq N.mul 1 N.mul_1_l N.mul_1_r.
+  #[export] Instance aac_N_lcm_1_Unit : Unit eq N.lcm (1)%N :=
+    Build_Unit eq N.lcm 1 N.lcm_1_l N.lcm_1_r.
   #[export] Instance aac_N_add_0_Unit : Unit eq N.add (0)%N :=
-    Build_Unit eq N.add (0)%N N.add_0_l N.add_0_r.
+    Build_Unit eq N.add 0 N.add_0_l N.add_0_r.
   #[export] Instance aac_N_max_0_Unit : Unit eq N.max 0 :=
     Build_Unit eq N.max 0 N.max_0_l N.max_0_r.
+  #[export] Instance aac_N_gcd_0_Unit : Unit eq N.gcd 0 :=
+    Build_Unit eq N.gcd 0 N.gcd_0_l N.gcd_0_r.
 
   (* We also provide liftings from [N.le] to [eq] *)
   #[export] Instance N_le_PreOrder : PreOrder N.le :=
diff --git a/theories/Tutorial.v b/theories/Tutorial.v
index 9eba645..290ef65 100644
--- a/theories/Tutorial.v
+++ b/theories/Tutorial.v
@@ -356,7 +356,7 @@ End Peano.
 
 Section AAC_normalise.
   Import Instances.Z.
-  Import ZArith.
+  Import ZArith Lia.
   Open Scope Z_scope.
  
   Variable a b c d : Z.
@@ -364,11 +364,31 @@ Section AAC_normalise.
     aac_normalise.
   Abort.
 
+  Goal b + 0 + a = c*1 -> a+b = c.
+    intro H.
+    aac_normalise in H.
+    assumption.
+  Qed.
+
+  Goal b + 0 + a = c*1+d -> a+b = d*(1+0)+c.
+    intro.
+    aac_normalise in *.
+    assumption.
+  Qed.
+  
   Goal Z.max (a+b) (b+a) = a+b.
     aac_reflexivity.
-    Show Proof.
   Abort.
 
+  (** Example by Abhishek Anand extracted from verification of a C++ gcd function *)
+  Goal forall a b a' b' : Z,
+    0 < b' -> Z.gcd a' b' = Z.gcd a b -> Z.gcd b' (a' mod b') = Z.gcd a b.
+  Proof.
+    intros.
+    aac_rewrite Z.gcd_mod; try lia.
+    aac_normalise_all.
+    lia.
+  Qed.
 End AAC_normalise.
 
 (** ** Examples from previous website *)
diff --git a/theories/Utils.v b/theories/Utils.v
index 2ba81e2..d290a48 100644
--- a/theories/Utils.v
+++ b/theories/Utils.v
@@ -30,19 +30,6 @@ Fixpoint eq_idx_bool i j :=
     | _, _ => false
   end.
 
-Fixpoint idx_compare i j :=
-  match i,j with
-    | xH, xH => Eq
-    | xH, _ => Lt
-    | _, xH => Gt
-    | xO i, xO j => idx_compare i j
-    | xI i, xI j => idx_compare i j
-    | xI _, xO _ => Gt
-    | xO _, xI _ => Lt
-  end.
-
-Notation pos_compare := idx_compare (only parsing).
-
 (** Specification predicate for boolean binary functions *)
 Inductive decide_spec {A} {B} (R : A -> B -> Prop) (x : A) (y : B) : bool -> Prop :=
 | decide_true : R x y -> decide_spec R x y true
@@ -64,16 +51,16 @@ Inductive compare_weak_spec A: A -> A -> comparison -> Prop :=
 | pcws_lt: forall i j, compare_weak_spec i j Lt
 | pcws_gt: forall i j, compare_weak_spec i j Gt.
 
-Lemma pos_compare_weak_spec: forall i j, compare_weak_spec i j (pos_compare i j).
+Lemma pos_compare_weak_spec: forall i j, compare_weak_spec i j (Pos.compare i j).
 Proof.
-  induction i; destruct j; simpl; try constructor;
-    case (IHi j); intros; constructor.
+  intros. case Pos.compare_spec; try constructor.
+  intros <-; constructor.
 Qed.
 
-Lemma idx_compare_reflect_eq: forall i j, idx_compare i j = Eq -> i=j.
+Lemma pos_compare_reflect_eq: forall i j, Pos.compare i j = Eq -> i=j.
 Proof.
-  intros i j.
-  case (pos_compare_weak_spec i j); intros; congruence.
+  intros ??.
+  case pos_compare_weak_spec; intros; congruence.
 Qed.
 
 (** ** Dependent types utilities *)
@@ -161,7 +148,7 @@ Section lists.
     list_compare (fun un vm =>
       let '(u,n) := un in
       let '(v,m) := vm in
-      lex (compare u v) (pos_compare n m)).
+      lex (compare u v) (Pos.compare n m)).
 
   Section list_compare_weak_spec.
     Variable A: Type.