proposition: Lemma spec_compare_mn_1: forall n x y, compare_mn_1 n x y = Z.compare (double_to_Z n x) (w_to_Z y).
proof: Proof. intros n; elim n; simpl; auto; clear n. intros n Hrec x; case x; clear x; auto. intros y; rewrite spec_compare; rewrite w_to_Z_0. reflexivity. intros xh xl y; simpl; rewrite spec_compare0_mn, Hrec. case Z.compare_spec. intros H1b. rewrite <- H1b; rewrite Z.mul_0_l; rewrite Z.add_0_l; auto. symmetry. apply Z.lt_gt. case (double_wB_lt n y); intros _ H0. apply Z.lt_le_trans with (1:= H0). fold double_wB. case (double_to_Z_pos n xl); intros H1 H2. apply Z.le_trans with (double_to_Z n xh * double_wB n). 2: auto with zarith. apply Z.le_trans with (1 * double_wB n); auto with zarith. case (double_to_Z_pos n xh); intros; exfalso; lia. Qed.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic