proposition: Theorem gpow_support_aux_not_e: forall n m p, 0 <= m -> m < p < m + Z_of_nat (length (support_aux (gpow m) n)) -> gpow p <> G.(e).
proof: Proof. intros n; elim n; simpl. intros m p Hm (H1, H2); contradict H2; auto with zarith. intros n1 Rec m p Hm; case (A_dec (op a (gpow m)) G.(e)); simpl. intros _ (H1, H2); contradict H2; auto with zarith. assert (tmp: forall p, Zpos (P_of_succ_nat p) = 1 + Z_of_nat p). intros p1; apply trans_equal with (Z_of_nat (S p1)); auto; rewrite inj_S; auto with zarith. rewrite tmp. intros H1 (H2, H3); case (Zle_lt_or_eq (1 + m) p); auto with zarith; intros H4; subst. apply (Rec (1 + m)); try split; auto with zarith. rewrite gpow_add; auto with zarith. rewrite gpow_1; auto with zarith. rewrite gpow_add; try rewrite gpow_1; auto with zarith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange