proposition: Theorem beq_nat_sym : forall (n m : nat), beq_nat n m = beq_nat m n.
proof: Proof. induction n; sp. unfold beq_nat; destruct m; sp. simpl; destruct m; simpl; sp. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega