proposition: Theorem pos_left_right_rect : forall p, P p.
proof: Proof. Proof using HP1 HP2. intros p. rewrite <- pos_lr_both. generalize (pos_both n m p); clear p; intros [|]; simpl; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)