proposition: Lemma eq_rlshift m n i j : (@rshift m n i == @lshift m n j) = false.
proof: Proof. by rewrite eq_sym eq_lrshift. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)