proposition: Fact pos_lr_both n m p : pos_lr (@pos_both n m p) = p.
proof: Proof. revert p; induction n as [ | n IHn ]; intros p; auto. simpl in p; pos_inv p; simpl; auto. specialize (IHn p). destruct (pos_both n m p); simpl in *; f_equal; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)