proposition: Theorem isupport_aux_is_inv_true: forall l a, In a (isupport_aux l) -> is_inv a = true.
proof: Proof. intros l a; elim l; simpl; auto. intros b l1 H; case_eq (is_inv b); intros H1; simpl; auto. intros [H2 | H2]; subst; auto. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup