proposition: Lemma scal_wf: forall n x sc, wfe x -> wft sc -> wfe (fst (scal sc x n)) /\ wft (snd (scal sc x n)).
proof: Proof. intros n; exact (scalb_wf n false). Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod