proposition: Lemma scal_list_correct: forall l sc a1 p1, a1 =~~= p1 -> [[scal_list sc a1 l]] -> fst (scal_list sc a1 l) =~~= EGroup.gpow p1 pG (Zmull l).
proof: Proof. assert (F0: forall p1, List.In p1 (FGroup.s pG)). intros p1. apply (FELLK_in pell_theory _ (in_all_znz _ p_pos)). intros l; elim l; auto; clear l. intros sc a1 p1 H H1. change (Zmull List.nil) with (1%positive). rewrite gpow_1; auto. intros a l Hrec sc a1 p1 H1 H2. rewrite Zmull_cons. rewrite Zpos_mult_morphism. rewrite gpow_gpow; auto with zarith. unfold scal_list; simpl List.fold_left. case_eq (scal sc a1 a); intros a2 sc2 Ha2. change (equiv (fst (scal_list sc2 a2 l)) (gpow (gpow p1 pG a) pG (Zmull l))). apply Hrec. change a2 with (fst (a2, sc2)). rewrite <- Ha2. apply scal_correct; auto. case (nInversible_scal_list sc2 a2 l); auto. unfold scal_list; simpl; rewrite <- Ha2; auto. intros; rewrite Ha2. inversion_clear H; constructor; repeat itac; auto. unfold scal_list; simpl; rewrite <- Ha2; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod