proposition: Theorem isupport_is_inv_true: forall a, In a isupport -> is_inv a = true.
proof: Proof. unfold isupport; intros a H; apply isupport_aux_is_inv_true with (1 := H). Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup