proposition: Lemma spec_get_endn: forall n m x y, eval n m x <= [mk_t n y] -> [mk_t n (DoubleBase.get_low (zeron n) m x)] = eval n m x.
proof: Proof. intros n m x y H. unfold eval. rewrite nmake_double. rewrite spec_mk_t in *. apply DoubleBase.spec_get_low. apply spec_zeron. exact ZnZ.spec_to_Z. apply Z.le_lt_trans with (ZnZ.to_Z y); auto. rewrite <- nmake_double; auto. case (ZnZ.spec_to_Z y); auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen