proposition: Theorem Theorem_4_5 (alpha: T1)(Halpha : nf alpha) (A B : list nat) (HA : Sorted Peano.lt A) (HB : Sorted Peano.lt B) (HAB : incl A B) : largeS alpha A -> largeS alpha B.
proof: Proof. intro H; destruct (incl_decomp A B HA HB HAB) as [C [D [H1 H2]]];auto. subst B; rewrite largeS_iff in *; eapply Lemma_4_5_2 with A;auto. rewrite sorted_ge_iff; split;auto. clear HA H H2 HB HAB; induction A; constructor;auto with arith. rewrite sorted_ge_iff; split; auto. generalize (C++D); intro E; induction E; constructor;auto with arith. now rewrite largeS_iff in *. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)