proposition: Lemma eqb_ord_rrshift n m i j: eqb_ord (@rshift n m i) (@rshift n m j) = eqb_ord i j.
proof: Proof. destruct i as [i Hi]; destruct j as [j Hj]. unfold eqb_ord. simpl. do 2 case eqb_spec; trivial. intros E E'. elim E. eapply Nat.add_cancel_l, E'. congruence. Qed.
imports: List PeanoNat common comparisons