proposition: Theorem is_inv_false: forall b, (forall a, (In a support) -> op b a <> e \/ op a b <> e) -> is_inv b = false.
proof: Proof. intros b H; unfold is_inv; apply is_inv_aux_false; auto. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup