proposition: Lemma add_add1_correct m n : [m + n] = ([m] + [n])%Z /\ [m +1 n] = ([m] + [n] + 1)%Z.
proof: Proof. generalize n; clear n. induction m as [ | a m Hrec]; nrom; auto. intros n; simpl; rewrite incr_correct; auto. intros n; destruct n as [ | b n]. unfold add_num; fold add_num; unfold add1_num; fold add1_num; rewrite incr_correct; auto with zarith. split. change ((a :: m) + (b :: n)) with (let c := (a + b)%uint63 in match c ?= a with | Lt => c::add1_num m n | _ => c::add_num m n end). lazy zeta; generalize (add_cp a b); rewrite compare_spec; case Z.compare_spec; nrom; intros HH H; case (Hrec n); intros H1 H2; try rewrite H; try rewrite H1; try rewrite H2; ring. change ((a :: m) +1 (b :: n)) with (let c := (1 + (a + b))%uint63 in match c ?= a with | Gt => c::add_num m n | _ => c::add1_num m n end). lazy zeta; generalize (add2_cp a b); rewrite compare_spec; case Z.compare_spec; nrom; intros HH H1; case (Hrec n); intros Hr1 Hr2; rewrite H1; (rewrite Hr1 || rewrite Hr2); ring. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63