proposition: Lemma rev_ordK {n} : involutive (@rev_ord n).
proof: Proof. by case: n => [|n] [i lti] //; apply: val_inj; rewrite /= !subSS subKn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)