proposition: Lemma positive_eq_correct p1 p2 : if positive_eq p1 p2 then p1 = p2 else p1 <> p2.
proof: Proof. revert p2; elim p1; [intros p3 Hrec | intros p3 Hrec|]; intros p2; (case p2; [intros p4 | intros p4 |]); simpl; try (intros HH; discriminate HH); auto; generalize (Hrec p4); case positive_eq; intros HH; try (subst p3; auto; fail); intros HH1; case HH; injection HH1; auto. Qed.
imports: ZArith List