proposition: Theorem inv_aux_prop_l: forall l a, is_inv_aux l a = true -> op (inv_aux l a) a = e.
proof: Proof. intros l a; elim l; simpl. intros; discriminate. intros b l1 H1; case (A_dec (op a b) e); case (A_dec (op b a) e); intros H3 H4; subst; auto. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup