proposition: Lemma scal_list_correct: forall l x sc, wfe x -> wft sc -> e2E (fst (scal_list sc x l)) = fst (ZEll.scal_list exx.(vN) exx.(vA) (z2Z sc) (e2E x) l)/\ z2Z (snd (scal_list sc x l)) = snd (ZEll.scal_list exx.(vN) exx.(vA) (z2Z sc) (e2E x) l).
proof: Proof. intros l1; elim l1; simpl; auto. unfold scal_list, ZEll.scal_list; simpl; intros a l2 Hrec x sc H1 H2. generalize (scal_correct a _ H1 H2) (scal_wf a _ H1 H2); case scal. case ZEll.scal; intros r1 rsc1; simpl. simpl; intros a1 sc1 (H3, H4) (H5, H6); subst r1 rsc1; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod