proposition: Lemma eqb_ord_lrshift n m i j: eqb_ord (@lshift n m i) (@rshift n m j) = false.
proof: Proof. destruct i as [i Hi]; destruct j as [j Hj]. unfold eqb_ord. simpl. case eqb_spec; trivial. intro E. rewrite E in Hi. rewrite leb_plus_r in Hi. discriminate. Qed.
imports: List PeanoNat common comparisons