fact: Fixpoint inv_aux (l: list A) (a: A) {struct l}: A := match l with nil => e | cons b l1 => if A_dec (op a b) e then if (A_dec (op b a) e) then b else inv_aux l1 a else inv_aux l1 a end.
imports: ZArith Tactic Wf_nat UList ListAux FGroup