proposition: Lemma scalb_correct: forall n b x sc, wfe x -> wft sc -> e2E (fst (scalb sc b x n)) = fst (ZEll.scalb exx.(vN) exx.(vA) (z2Z sc) b (e2E x) n)/\ z2Z (snd (scalb sc b x n)) = snd (ZEll.scalb exx.(vN) exx.(vA) (z2Z sc) b (e2E x) n).
proof: Proof. intros n; elim n; clear n; auto. intros p Hrec b x sc H1 H2. case b; unfold scalb; fold scalb. generalize (scalb_wf p true x H1 H2); generalize (Hrec true _ _ H1 H2); case scalb; simpl. case ZEll.scalb; intros r1 rc1; simpl. intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. apply ndouble_correct; auto. generalize (scalb_wf p true x H1 H2); generalize (Hrec true _ _ H1 H2); case scalb; simpl. case ZEll.scalb; intros r1 rc1; simpl. intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. generalize (ndouble_wf _ H5 H6); generalize (ndouble_correct _ H5 H6); case ndouble; simpl. case ZEll.ndouble; intros r1 rc1; simpl. intros a3 sc3 (H7,H8) (H9,H10); subst r1 rc1. replace (ZEll.nopp (vN exx) (e2E x)) with (e2E (nopp x)). apply nadd_correct; auto. generalize H1; case x; auto. intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto. rewrite nopp_correct; auto. apply f_equal2 with (f := ZEll.nopp); auto. generalize H1; case x; simpl; auto; clear x H1. intros x1 y1 z1 [HH1 [HH2 HH3]]; apply f_equal3 with (f := ZEll.ntriple); auto. repeat rewrite nsubz; auto. rewrite zc0. unfold ZEll.nsub; simpl. rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith. rewrite <- Zopp_mult_distr_l. rewrite <- Zopp_plus_distr. rewrite Zmult_comm; rewrite Zplus_comm. rewrite <- Z_div_mod_eq_full. rewrite Z.opp_involutive; rewrite <- z2ZN. apply sym_equal; auto. generalize H1; case x; auto. intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto. intros p Hrec b x sc H1 H2. case b; unfold scalb; fold scalb. generalize (scalb_wf p false x H1 H2); generalize (Hrec false _ _ H1 H2); case scalb; simpl. case ZEll.scalb; intros r1 rc1; simpl. intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. generalize (ndouble_wf _ H5 H6); generalize (ndouble_correct _ H5 H6); case ndouble; simpl. case ZEll.ndouble; intros r1 rc1; simpl. intros a3 sc3 (H7,H8) (H9,H10); subst r1 rc1. replace (ZEll.nopp (vN exx) (e2E x)) with (e2E (nopp x)). apply nadd_correct; auto. rewrite nopp_correct; auto. apply f_equal2 with (f := ZEll.nopp); auto. generalize H1; case x; simpl; auto; clear x H1. intros x1 y1 z1 [HH1 [HH2 HH3]]; apply f_equal3 with (f := ZEll.ntriple); auto. repeat rewrite nsubz; auto. rewrite zc0. unfold ZEll.nsub; simpl. rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith. rewrite <- Zopp_mult_distr_l. rewrite <- Zopp_plus_distr. rewrite Zmult_comm; rewrite Zplus_comm. rewrite <- Z_div_mod_eq_full. rewrite Z.opp_involutive; rewrite <- z2ZN. apply sym_equal; auto. generalize H1; case x; auto. intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto. generalize (scalb_wf p false x H1 H2); generalize (Hrec false _ _ H1 H2); case scalb; simpl. case ZEll.scalb; intros r1 rc1; simpl. intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. apply ndouble_correct; auto. intros b x sc H H1. case b; simpl; auto. apply ndouble_correct; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod