proposition: Lemma beq_pos_ok : forall x y, beq_pos x y = true <-> x = y.
proof: Proof. induction x; destruct y; simpl; intros; try (intuition; discr). rewrite IHx. intuition. subst. refl. inversion H. refl. rewrite IHx. intuition. subst. refl. inversion H. refl. Qed.
imports: CoLoR(LogicUtil) Coq(Lia)