proposition: Lemma split_subproof m n (i : 'I_(m + n)) : i >= m -> i - m < n.
proof: Proof. by move/subSn <-; rewrite leq_subLR. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)