proposition: Lemma eq_lshift m n i j : (@lshift m n i == @lshift m n j) = (i == j).
proof: Proof. by rewrite (inj_eq (@lshift_inj _ _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)