proposition: Fact pos_left_right_neq n m p q : @pos_left n m p <> @pos_right n m q.
proof: Proof. intros H. apply f_equal with (f := @pos_both _ _) in H. now rewrite pos_both_left, pos_both_right in H. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)