fact: Fixpoint support_aux (b: A) (n: nat) {struct n}: list A := b::let c := op a b in match n with O => nil | (S n1) =>if A_dec c G.(e) then nil else support_aux c n1 end.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange