proposition: Lemma cast_ordKV n1 n2 eq_n : cancel (cast_ord (esym eq_n)) (@cast_ord n1 n2 eq_n).
proof: Proof. by move=> i; apply: val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)