proposition: Lemma ord_predK n : cancel (@ord_pred n) (@ordS n).
proof: Proof. move=> [[|i] ilt]; apply/val_inj => /=. by rewrite [n.-1 %% n]modn_small// prednK// modnn. by rewrite modnDr [i %% n]modn_small ?modn_small// ltnW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)