proposition: Lemma cast_ord_comp n1 n2 n3 eq_n2 eq_n3 i : @cast_ord n2 n3 eq_n3 (@cast_ord n1 n2 eq_n2 i) = cast_ord (etrans eq_n2 eq_n3) i.
proof: Proof. exact: val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)