proposition: Theorem inv_aux_inv: forall l a b, op a b = e -> op b a = e -> (In a l) -> is_inv_aux l b = true.
proof: Proof. intros l a b; elim l; simpl. intros _ _ H; case H. intros c l1 Rec H H0 H1; case H1; clear H1; intros H1. subst c. case (A_dec (op b a) e); case (A_dec (op a b) e); auto. case (A_dec (op b c) e); case (A_dec (op c b) e); auto. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup