proposition: Lemma ordSK n : cancel (@ordS n) (@ord_pred n).
proof: Proof. move=> [i ilt]; apply/val_inj => /=. case: (ltngtP i.+1) (ilt) => // [Silt|<-]; last by rewrite modnn/= modn_small. by rewrite [i.+1 %% n]modn_small// addSn/= modnDr modn_small. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)