proposition: Lemma eq_pos_spec : forall n m, reflect (n=m) (eq_pos_bool n m).
proof: Proof. induction n; intros [m|m|]; simpl; try constructor; try congruence. case (IHn m); intro; subst; constructor; congruence. case (IHn m); intro; subst; constructor; congruence. Qed.
imports: ATBR(Common) Coq(Equality Program Sumbool Peano)