proposition: Fact pos_both_right n m p : @pos_both n m (@pos_right n m p) = inr p.
proof: Proof. revert p; induction n as [ | n IHn]; intros p; simpl; auto. rewrite IHn; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)