proposition: Theorem gpow_evaln: forall n, 0 < n -> exists p, (length p <= Z.abs_nat n)%nat /\ (forall i, In i p -> In i support) /\ forall x, In x IA.(s) -> eval A plus mult zero (zero::p) x = gpow x IA n.
proof: Proof. intros n Hn; generalize Hn; pattern n; apply natlike_ind; auto with zarith. intros H1; contradict H1; auto with zarith. intros x Hx Rec _. case Zle_lt_or_eq with (1 := Hx); clear Hx; intros Hx; subst; simpl. case Rec; auto; simpl; intros p (Hp1, (Hp2, Hp3)); clear Rec. exists (zero::p); split; simpl. rewrite Zabs_nat_Zsucc; auto with arith zarith. split. intros i [Hi | Hi]; try rewrite <- Hi; auto. intros x1 Hx1; simpl. rewrite Hp3; repeat rewrite plus_zero; unfold Z.succ ; try rewrite gpow_add; auto with zarith. rewrite gpow_1; try apply mult_comm; auto. apply (fun x => isupport_incl _ mult support e A_dec x); auto. change (In (gpow x1 IA x) IA.(s)). apply gpow_in; auto. apply mult_internal; auto. apply (fun x => isupport_incl _ mult support e A_dec x); auto. change (In (gpow x1 IA x) IA.(s)). apply gpow_in; auto. exists (e:: nil); split; simpl. compute; auto with arith. split. intros i [Hi | Hi]; try rewrite <- Hi; auto; case Hi. intros x Hx; simpl. rewrite plus_zero; rewrite (fun x => mult_comm x zero); try rewrite mult_zero; auto. rewrite plus_comm; try rewrite plus_zero; auto. Qed.
imports: ZCAux List Root UList IGroup EGroup FGroup