proposition: Lemma spec_compare0_mn: forall n x, compare0_mn n x = (0 ?= double_to_Z n x).
proof: Proof. intros n; elim n; clear n; auto. intros x; rewrite spec_compare0_m; rewrite w_to_Z_0; auto. intros n Hrec x; case x; unfold compare0_mn; fold compare0_mn; auto. fold word in *. intros xh xl. rewrite 2 Hrec. simpl double_to_Z. set (wB := DoubleBase.double_wB wm_base n). case Z.compare_spec; intros Cmp. rewrite <- Cmp. reflexivity. symmetry. apply Z.gt_lt, Z.lt_gt. assert (0 < wB). unfold wB, DoubleBase.double_wB, base; auto with zarith. change 0 with (0 + 0); apply Z.add_lt_le_mono. apply Z.mul_pos_pos; auto with zarith. case (double_to_Z_pos n xl); auto with zarith. case (double_to_Z_pos n xh); intros; exfalso; lia. Qed.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic