+theorem eqb_n_n: \forall n. eqb n n = true.
+intro.elim n.simplify.reflexivity.
+simplify.assumption.
+qed.
+
+theorem eq_to_eqb_true: \forall n,m:nat.
+n = m \to eqb n m = true.
+intros.apply eqb_elim n m.
+intros. reflexivity.
+intros.apply False_ind.apply H1 H.
+qed.
+
+theorem not_eq_to_eqb_false: \forall n,m:nat.
+\lnot (n = m) \to eqb n m = false.
+intros.apply eqb_elim n m.
+intros. apply False_ind.apply H H1.
+intros.reflexivity.
+qed.
+