proposition: Lemma spec_ww_compare : forall x y, ww_compare x y = Z.compare [[x]] [[y]].
proof: Proof. destruct x as [ |xh xl];destruct y as [ |yh yl];simpl;trivial. rewrite 2 spec_w_compare, spec_w_0. destruct (Z.compare_spec 0 [|yh|]) as [H|H|H]. rewrite <- H;simpl. reflexivity. symmetry. change (0 < [|yh|]*wB+[|yl|]). change 0 with (0*wB+0). rewrite <- spec_w_0 at 2. apply wB_lex_inv;trivial. absurd (0 <= [|yh|]). apply Z.lt_nge; trivial. destruct (spec_to_Z yh);trivial. rewrite 2 spec_w_compare, spec_w_0. destruct (Z.compare_spec [|xh|] 0) as [H|H|H]. rewrite H;simpl;reflexivity. absurd (0 <= [|xh|]). apply Z.lt_nge; trivial. destruct (spec_to_Z xh);trivial. comp2ord. change 0 with (0*wB+0). rewrite <- spec_w_0 at 2. apply wB_lex_inv;trivial. rewrite 2 spec_w_compare. destruct (Z.compare_spec [|xh|] [|yh|]) as [H|H|H]. rewrite H. symmetry. apply Z.add_compare_mono_l. comp2ord. apply wB_lex_inv;trivial. comp2ord. apply wB_lex_inv;trivial. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType