proposition: Lemma lshift_subproof m n (i : 'I_m) : i < m + n.
proof: Proof. by apply: leq_trans (valP i) _; apply: leq_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)