proposition: Theorem optimize_0plus_b_sound : forall b, beval (optimize_0plus_b b) = beval b.
proof: Proof. Admitted. Tactic Notation "simpl_and_try" tactic(c) := simpl; try c. Example silly_presburger_example : forall m n o p, m + n <= n + o /\ o + 3 = p + 3 -> m <= p. Proof. intros. omega. Qed.
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps