proposition: Theorem support_aux_length_le: forall n a, (length (support_aux a n) <= n + 1)%nat.
proof: Proof. intros n; elim n; simpl; auto. intros n1 Rec a1; case (A_dec (op a a1) G.(e)); simpl; auto with arith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange