proposition: Theorem not_all_solutions: forall i, 0 < i < g_order IA -> exists a, In a IA.(s) /\ gpow a IA i <> e.
proof: Proof. intros i (Hi, Hi2). case (check_list_gpow IA.(s) i); try intros H; auto with datatypes. case (gpow_evaln i); auto; intros p (Hp1, (Hp2, Hp3)). absurd ((op e) = zero). intros H1; case e_not_zero. rewrite <- (plus_op_zero e); try rewrite H1; auto. rewrite plus_comm; auto. apply (root_max_is_zero _ (fun x => In x support) plus mult op zero) with (l := IA.(s)) (p := op e :: p); auto with datatypes. simpl; intros x [Hx | Hx]; try rewrite <- Hx; auto. intros x Hx. generalize (Hp3 _ Hx); simpl; rewrite plus_zero; auto. intros tmp; rewrite tmp; clear tmp. rewrite H; auto; rewrite plus_comm; auto with datatypes. apply mult_internal; auto. apply eval_P; auto. simpl; apply Nat.le_succ_l; apply Nat.le_lt_trans with (1 := Hp1). apply inj_lt_inv. rewrite inj_Zabs_nat; auto with zarith. rewrite Z.abs_eq ; auto with zarith. Qed.
imports: ZCAux List Root UList IGroup EGroup FGroup