proposition: Theorem support_aux_ulist: forall n m, 0 <= m -> (forall p, 0 <= p < m -> gpow (1 + p) <> G.(e)) -> ulist (support_aux (gpow m) n).
proof: Proof. intros n; elim n; auto; clear n. intros m _ _; auto. simpl; apply ulist_cons; auto. intros n1 Rec m Hm H. simpl; case (A_dec (op a (gpow m)) G.(e)); auto. intros He; apply ulist_cons; auto. intros H1; case (support_aux_gpow n1 (1 + m) (gpow m)); auto with zarith. rewrite gpow_add; try rewrite gpow_1; auto with zarith. intros p (Hp1, Hp2). assert (H2: gpow (1 + Z_of_nat p) = G.(e)). apply gpow_i with m; auto with zarith. rewrite Hp2; eq_tac; auto with zarith. case (Zle_or_lt m (Z_of_nat p)); intros H3; auto. 2: case (H (Z_of_nat p)); auto with zarith. case (support_aux_not_e (S n1) m (gpow (1 + Z_of_nat p))); auto. rewrite gpow_add; auto with zarith; simpl; rewrite e_is_zero_r; auto. case (A_dec (op a (gpow m)) G.(e)); auto. intros _; rewrite <- gpow_1; repeat rewrite <- gpow_add; auto with zarith. replace (1 + Z_of_nat p) with ((1 + m) + (Z_of_nat (p - Z.abs_nat m))). apply support_aux_in; auto with zarith. 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. rewrite <- gpow_1; repeat rewrite <- gpow_add; auto with zarith. apply (Rec (1 + m)); auto with zarith. intros p H1; case (Zle_lt_or_eq p m); intros; subst; auto with zarith. rewrite gpow_add; auto with zarith. rewrite gpow_1; auto. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange