proposition: Lemma scalL_not_1: forall l sc a p1 n, a =~~= p1 -> [[scalL sc a l]] -> List.In n l -> gpow p1 pG (Zmull l / n) <> pG.(FGroup.e).
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 (List.In). intros a l Hrec sc a1 p1 n H H1 [H2 | H2]; subst. case (nInversible_scalL _ _ _ H1); intros H3 H4. rewrite Zmull_cons. repeat rewrite Zpos_mult_morphism. rewrite (Zmult_comm n). repeat rewrite Z_div_mult; auto. generalize H1; simpl scalL. case scal. intros n1 sc1. generalize (@scal_list_correct l sc1 a1 p1 H). case scal_list. intros n2; case n2; clear n2. intros z2 _ HH; inversion HH; case inversible_0; auto. intros x1 y1 z1 sc2 H5 H6 H7. rewrite H7 in H5. simpl fst in H5. case (nInversible_scalL _ _ _ H6); intros H8 H9. absurd (ntriple x1 y1 z1 =~~= FGroup.e pG). intros HH; inversion HH. apply H5; constructor; auto. red; simpl; auto. rewrite Zmull_cons; auto. repeat rewrite Zpos_mult_morphism. case (nInversible_scalL _ _ _ H1); intros U1 U2. rewrite (Zmull_div n); auto. rewrite Zmult_assoc. rewrite Z_div_mult; auto. rewrite gpow_gpow; auto. case (nInversible_scalL _ _ _ H1); auto. intros H3 H4. simpl in H1; revert H1. 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 (sc2 ** z1)%Z n1); 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. red; simpl; auto; intros HH; discriminate. apply Z.ge_le; apply Z_div_ge0; red; simpl; auto; intros HH; discriminate. red; simpl; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod