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