proposition: Lemma scalL_1: forall l sc a p1, a =~~= p1 -> [[scalL sc a l]] -> fst (scalL sc a l) =~~= 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. simpl scalL; simpl fst; simpl Zmull. unfold Zmull; simpl List.fold_left. intros; rewrite gpow_1; auto. intros a l Hrec sc a1 p1 H1 H2. rewrite Zmull_cons. repeat rewrite Zpos_mult_morphism. rewrite gpow_gpow; auto. 2: red;simpl; auto; intros HH; discriminate. 2: red;simpl; auto; intros HH; discriminate. simpl in H2; revert H2; simpl scalL. case_eq (scal sc a1 a). intros n1 sc1 Hn1. case_eq (scal_list sc1 a1 l). intros n2 sc2; case n2. intros _ HH; inversion HH. case inversible_0; auto. intros x1 y1 z1 Hn2 H5. apply Hrec; auto. change n1 with (fst (n1, sc1)). rewrite <- Hn1. apply scal_correct; auto. case (nInversible_scalL _ _ _ H5). intros H6 H7. case (nInversible_scal_list sc1 a1 l). rewrite Hn2; constructor; auto. intros H8 H9. rewrite Hn1; inversion H6; constructor; auto; repeat itac. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod