proposition: Theorem support_aux_in: forall n m p, 0 <= m -> (p < length (support_aux (gpow m) n))% nat -> (In (gpow (m + Z_of_nat p)) (support_aux (gpow m) n)).
proof: Proof. intros n; elim n; simpl; auto; clear n. intros m p Hm H1; replace p with 0%nat. left; eq_tac; auto with zarith. generalize H1; case p; simpl; auto with arith. intros n H2; contradict H2; apply Nat.le_ngt; auto with arith. intros n1 Rec m p Hm; case (A_dec (op a (gpow m)) G.(e)); simpl; intros H1 H2; auto. replace p with 0%nat. left; eq_tac; auto with zarith. generalize H2; case p; simpl; auto with arith. intros n H3; contradict H3; apply Nat.le_ngt; auto with arith. generalize H2; case p; simpl; clear H2. rewrite Zplus_0_r; auto. intros n. 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; clear tmp. rewrite <- gpow_1; rewrite <- gpow_add; auto with zarith. rewrite Zplus_assoc; rewrite (Zplus_comm 1); intros H2; right; apply Rec; auto with zarith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange