proposition: Lemma beq_Z_ok : forall x y, beq_Z x y = true <-> x = y.
proof: Proof. intros [] []; simpl; split. 1-2: reflexivity. 1-6, 9-14: discriminate. all: rewrite beq_pos_ok; intros H; inversion H; reflexivity. Qed.
imports: CoLoR(LogicUtil) Coq(Lia)