proposition: Lemma scal_list_wf: forall l x sc, wfe x -> wft sc -> wfe (fst (scal_list sc x l)) /\ wft (snd (scal_list sc x l)).
proof: Proof. intros l1; elim l1; simpl; auto. unfold scal_list; intros a l Hrec x sc H1 H2; simpl. generalize (@scal_wf a _ _ H1 H2); case (scal sc x a); simpl; intros x1 sc1 [H3 H4]; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod