proposition: Theorem support_aux_gpow: forall n m b, 0 <= m -> In b (support_aux (gpow m) n) -> exists p, (0 <= p < length (support_aux (gpow m) n))%nat /\ b = gpow (m + Z_of_nat p).
proof: Proof. intros n; elim n; simpl. intros n1 b Hm [H1 | H1]; exists 0%nat; simpl; rewrite Zplus_0_r; auto; case H1. intros n1 Rec m b Hm [H1 | H1]. exists 0%nat; simpl; rewrite Zplus_0_r; auto; auto with arith. generalize H1; case (A_dec (op a (gpow m)) G.(e)); clear H1; simpl; intros H1 H2. case H2. case (Rec (1 + m) b); auto with zarith. rewrite gpow_add; auto with zarith. rewrite gpow_1; auto. intros p (Hp1, Hp2); exists (S p); split; auto with zarith. rewrite <- gpow_1. rewrite <- gpow_add; auto with zarith. rewrite inj_S; rewrite Hp2; eq_tac; auto with zarith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange