proposition: Lemma base_lexi_order a b n1 n2 wB : (0 <= a < wB -> 0 <= b < wB -> match a + wB * n1 ?= b + wB * n2 with | Eq => a = b /\ n1 = n2 | Lt => n1 < n2 \/ (n1 = n2 /\ a < b) | Gt => n2 < n1 \/ (n1 = n2 /\ b < a) end)%Z.
proof: Proof. intros (Ha1, Ha2) (Hb1, Hb2). case Z.compare_spec; intros HH. case (Zle_or_lt n1 n2); intros H1. case (Zle_lt_or_eq _ _ H1); clear H1; intros H1; auto. assert (HH1: (wB + wB * (n2 - n1 -1) = (a - b))%Z). replace a with ((a + wB * n1) - wB * n1)%Z by ring. rewrite HH; ring. assert (Hu: (0 <= wB * (n2 - n1 - 1))%Z); auto with zarith. split; auto. replace a with ((a + wB * n1) - wB * n1)%Z by ring. rewrite HH, H1; ring. assert (wB + wB * (n1 - n2 -1) = (b - a))%Z. replace b with ((b + wB * n2) - wB * n2)%Z by ring. rewrite <-HH; ring. assert (Hu: (0 <= wB * (n1 - n2 - 1))%Z); auto with zarith. case (Zle_or_lt n2 n1); intros H1; auto. case (Zle_lt_or_eq _ _ H1); clear H1; intros H1; auto. assert (0 <= wB * (n1 - n2 - 1))%Z by auto with zarith. enough (wB + wB * (n1 - n2 -1) < (b - a))%Z by auto with zarith. repeat rewrite Zmult_minus_distr_l; rewrite Zmult_1_r; auto with zarith. rewrite H1 in HH; auto with zarith. case (Zle_or_lt n1 n2); intros H1; auto. case (Zle_lt_or_eq _ _ H1); clear H1; intros H1; auto. assert (0 <= wB * (n2 - n1 - 1))%Z by auto with zarith. enough (wB + wB * (n2 - n1 -1) < (a - b))%Z by auto with zarith. repeat rewrite Zmult_minus_distr_l; rewrite Zmult_1_r; auto with zarith. rewrite H1 in HH; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63