proposition: Lemma scalL_correct: forall l x sc, wfe x -> wft sc -> e2E (fst (scalL sc x l)) = fst (ZEll.scalL exx.(vN) exx.(vA) (z2Z sc) (e2E x) l)/\ z2Z (snd (scalL sc x l)) = snd (ZEll.scalL exx.(vN) exx.(vA) (z2Z sc) (e2E x) l).
proof: Proof. intros l1; elim l1; simpl; auto. intros a l2 Hrec x sc H1 H2. generalize (scal_wf a _ H1 H2) (scal_correct a _ H1 H2); case scal; simpl. case ZEll.scal; intros r1 rsc1; simpl. intros a1 sc1 (H3, H4) (H5, H6); subst r1 rsc1. generalize (scal_list_wf l2 _ H1 H4) (scal_list_correct l2 _ H1 H4); case scal_list; simpl. case ZEll.scal_list; intros r1 rsc1; simpl. intros a2 sc2 (H7, H8) (H9, H10); subst r1 rsc1. generalize H7; clear H7; case a2; simpl; auto. rewrite zc0; auto. intros x1 y1 z1 (V1, (V2, V3)); auto. generalize (nmulw H8 V3) (nmulz H8 V3); intros V4 V5; rewrite <- V5. apply Hrec; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod