proposition: Lemma scalb_wf: forall n b x sc, wfe x -> wft sc -> wfe (fst (scalb sc b x n)) /\ wft (snd (scalb sc b x n)).
proof: Proof. intros n; elim n; unfold scalb; fold scalb; auto. intros n1 Hrec b x sc H H1. case (Hrec true x sc H H1). case scalb; simpl fst; simpl snd. intros a1 sc1 H2 H3. case (ndouble_wf _ H2 H3); auto; case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. case b; auto. case (nadd_wf _ _ (nopp_wf _ H) H4 H5); auto; case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. intros n1 Hrec b x sc H H1. case (Hrec false x sc H H1). case scalb; simpl fst; simpl snd. intros a1 sc1 H2 H3. case (ndouble_wf _ H2 H3); auto; case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. case b; auto. case (nadd_wf _ _ H H4 H5); auto; case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. intros b x sc H H1; case b; auto. case (ndouble_wf _ H H1); auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod