proposition: Theorem support_internal: forall a b, In a support -> In b support -> In (op a b) support.
proof: Proof. intros a1 b1 H1 H2. case support_gpow with (1 := H1); auto; intros p1 ((H3, H4), H5); subst. case support_gpow with (1 := H2); auto; intros p2 ((H5, H6), H7); subst. rewrite <- gpow_add; auto with zarith. case gpow_1_more with (m:= p1 + p2) (2 := gpow_length_support_is_e); auto with zarith. intros p3 ((H8, H9), H10); rewrite H10; apply support_in; auto with zarith. Qed.
imports: ZArith Tactic List ZCAux ZArith Znumtheory Wf_nat UList FGroup Lagrange