proposition: Fact pos_not_diag_spec p q : In (p,q) pos_not_diag <-> p <> q.
proof: Proof. unfold pos_not_diag. rewrite filter_In; simpl. destruct (pos_eq_dec p q). split. intros (_ & ?); discriminate. intros []; auto. split; try tauto; split; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils)