proposition: Theorem isupport_length_strict: forall b, (In b support) -> (forall a, (In a support) -> op b a <> e \/ op a b <> e) -> (length isupport < length support)%nat.
proof: Proof. intros b H H1; apply ulist_incl_length_strict. apply isupport_ulist. apply isupport_incl. intros H2; case (isupport_aux_not_in b support); auto. Qed.
imports: ZArith Tactic Wf_nat UList ListAux FGroup