proposition: Lemma eq_int_corr : forall n m:Z, eq_int n m = true -> n = m.
proof: Proof. simple induction n; simple induction m; simpl in |- *; intros. trivial. inversion H. inversion H. inversion H. rewrite <- (convert_is_POS p). rewrite <- (convert_is_POS p0). cut (nat_of_P p = nat_of_P p0). auto. apply eq_nat_corr. assumption. inversion H. inversion H. inversion H. cut (p = p0); intros. rewrite H0; auto. rewrite (anti_convert_pred_convert p). rewrite (anti_convert_pred_convert p0). cut (nat_of_P p = nat_of_P p0). intro. auto. apply eq_nat_corr. assumption. Qed.
imports: CoRN.logic.CLogic Coq.Bool.Bool