proposition: Theorem inv_internal: forall a, In a isupport -> In (inv a) isupport.
proof: Proof. intros a H; apply isupport_is_in. apply is_inv_true with a; auto. apply inv_prop_l; auto. apply inv_prop_r; auto. apply (isupport_incl a); auto. case (inv_aux_in support a); unfold inv; auto. intros H1; rewrite H1; apply e_in_support; auto with zarith. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup