proposition: Theorem support_aux_not_e: forall n m b, 0 <= m -> In b (tail (support_aux (gpow m) n)) -> ~ b = G.(e).
proof: Proof. intros n; elim n; simpl. intros m b Hm H; case H. intros n1 Rec m b Hm; case (A_dec (op a (gpow m)) G.(e)); intros H1 H2; simpl; auto. assert (Hm1: 0 <= 1 + m); auto with zarith. generalize( Rec (1 + m) b Hm1) H2; case n1; auto; clear Hm1. intros _ [H3 | H3]; auto. contradict H1; subst; auto. rewrite gpow_add; simpl; try rewrite e_is_zero_r; auto with zarith. intros n2; case (A_dec (op a (op a (gpow m))) G.(e)); intros H3. intros _ [H4 | H4]. contradict H1; subst; auto. case H4. intros H4 [H5 | H5]; subst; auto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange