proposition: Theorem support_i_internal: forall a, In a support -> In (G.(i) a) support.
proof: Proof. generalize gpow_in; intros Hp. intros a1 H1. case support_gpow with (1 := H1); auto. intros p1 ((H2, H3), H4); case Zle_lt_or_eq with (1 := H2); clear H2; intros H2; subst. 2: rewrite gpow_0; rewrite i_e; apply support_in_e. replace (G.(i) (gpow p1)) with (gpow (Z_of_nat (length support - Z.abs_nat p1))). apply support_in. rewrite inj_minus1. rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. apply inj_le_rev; rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. apply g_cancel_l with (g:= G) (a := gpow p1); sauto. rewrite <- gpow_add; auto with zarith. replace (p1 + Z_of_nat (length support - Z.abs_nat p1)) with (Z_of_nat (length support)). rewrite gpow_length_support_is_e; sauto. rewrite inj_minus1. rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. apply inj_le_rev; rewrite inj_Zabs_nat. rewrite Z.abs_eq; auto with zarith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange