proposition: Theorem support_aux_length_le_is_e: forall n m, 0 <= m -> (length (support_aux (gpow m) n) <= n)%nat -> gpow (m + Z_of_nat (length (support_aux (gpow m) n))) = G.(e) .
proof: Proof. intros n; elim n; simpl; auto. intros m _ H1; contradict H1; auto with arith. intros n1 Rec m Hm; case (A_dec (op a (gpow m)) G.(e)); simpl; intros H1. intros H2; rewrite Zplus_comm; rewrite gpow_add; simpl; try rewrite e_is_zero_r; auto with zarith. 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; apply Rec; auto with zarith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange