proposition: Theorem inv_prop_r: forall a, In a isupport -> op a (inv a) = e.
proof: Proof. intros a H; unfold inv; apply inv_aux_prop_r with (l := support). change (is_inv a = true). apply isupport_is_inv_true; auto. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup