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