proposition: Lemma sub_sub1_correct m n : (([n] <= [m])%Z -> [m - n] = ([m] - [n])%Z) /\ ([n] < [m] -> [m -1 n] = [m] - (1 + [n]))%Z.
proof: Proof. generalize n; clear n. induction m as [ | a m Hrec]; nrom; auto. intros n; induction n as [ | b n Hrec]; unfold sub_num, sub1_num; fold sub_num; fold sub1_num; nrom; auto with zarith. generalize (to_Z_pos (b::n)); nrom; auto with zarith. intros n; destruct n as [ | b n]; unfold sub_num, sub1_num; fold sub_num; fold sub1_num; nrom; auto with zarith. split; intros H1; auto with zarith. rewrite decr_correct; auto with zarith. split; intros H1. case (Hrec n); intros H2 H3. assert (H4: ([n] <= [m])%Z). generalize (base_lexi_order _ _ [n] [m] _ (to_Z_bounded b) (to_Z_bounded a)); nrom; case (Zle_lt_or_eq _ _ H1); intros H4. red in H4; rewrite H4; auto with zarith. rewrite H4, Z.compare_refl; auto with zarith. generalize (sub_cp a b); rewrite compare_spec; case Z.compare_spec; nrom; intros HH0 HH1; rewrite HH1; try rewrite H2; auto; try ring. rewrite H3; try ring. case (Zle_lt_or_eq _ _ H4); intros H5; auto. rewrite H5 in H1 |- *. generalize (base_lexi_order _ _ [m] [m] _ (to_Z_bounded b) (to_Z_bounded a)); nrom. assert (H6: (to_Z a < to_Z b)%Z). case (Zle_or_lt (to_Z b) (to_Z a)); intros H6; auto. generalize HH1; rewrite sub_spec; nrom. case (to_Z_bounded a); nrom; intros Ha1 Ha2; case (to_Z_bounded b); nrom; intros Hb1 Hb2; rewrite Zmod_small; auto with zarith. case (Zle_lt_or_eq _ _ H1); intros H7. red in H7; rewrite H7; auto with zarith. rewrite H7, Z.compare_refl; auto with zarith. generalize (base_lexi_order _ _ [n] [m] _ (to_Z_bounded b) (to_Z_bounded a)); nrom. red in H1; rewrite H1. intros [H2 | (H2, H3)]. case (Hrec n); intros H3 H4. generalize (sub1_cp a b); rewrite compare_spec; case Z.compare_spec; nrom; intros HH0 HH1; rewrite HH1; try rewrite H3; try rewrite H4; auto with zarith; try ring. assert (Ha: (to_Z (a - (1 + b)) < to_Z a)%Z). case (to_Z_bounded a); nrom; intros H1a H2a. case (to_Z_bounded b); nrom; intros H1b _. rewrite sub_spec, Zmod_small; nrom; auto with zarith; rewrite add_spec, Zmod_small; nrom; auto with zarith. rewrite compare_spec; case Z.compare_spec; auto with zarith. intros _; case (Hrec n); intros H4 _; nrom. rewrite H4; auto with zarith. case (to_Z_bounded a); nrom; intros H1a H2a; case (to_Z_bounded b); nrom; intros H1b _; rewrite sub_spec, Zmod_small; nrom; auto with zarith; rewrite add_spec, Zmod_small; nrom; auto with zarith; try ring. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63