proposition: Theorem is_inv_true: forall a b, op b a = e -> op a b = e -> (In a support) -> is_inv b = true.
proof: Proof. intros a b H H1 H2; unfold is_inv; apply inv_aux_inv with a; auto. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup