proposition: Lemma eq_correct n1 n2 : if eq_num n1 n2 then [n1] = [n2]%Z else [n1] <> [n2]%Z.
proof: Proof. generalize n2; clear n2. induction n1 as [ | a n1 Hrec]. intros n2; generalize (zerop_correct n2); simpl; case zerop_num; auto. case (to_Z_bounded a); nrom; intros Ha1 Ha2. intros [ |b n2]; unfold eq_num; fold eq_num; nrom. generalize (zerop_correct (a::n1)); simpl; case zerop_num; auto. rewrite compare_spec; case Z.compare_spec; nrom; intros H1; try ( intros HH; generalize (base_lexi_order _ _ [n1] [n2] _ (to_Z_bounded a) (to_Z_bounded b)); nrom; rewrite HH, Z.compare_refl; intros (H3,H4); contradict H1; auto with zarith). generalize (Hrec n2); case eq_num; intros H2. apply Zcompare_Eq_eq; generalize (base_lexi_order _ _ [n1] [n2] _ (to_Z_bounded a) (to_Z_bounded b)); nrom; case Z.compare; auto. intros [H3 | (H3, H4)]; contradict H3; auto with zarith. intros [H3 | (H3, H4)]; contradict H3; auto with zarith. intros HH; generalize (base_lexi_order _ _ [n1] [n2] _ (to_Z_bounded a) (to_Z_bounded b)); nrom; rewrite HH, Z.compare_refl; intros (H3,H4); case H2; auto. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63