proposition: Lemma omega_mult_mlarge_0 i : forall k, mlarge (T1omega * (S i)) (interval (S k) (Nat.pred (iterate (fun p => S (2 * p)%nat) (S i) (S k)))).
proof: Proof. unfold mlarge; induction i. - simpl; intro k; replace (S (k + S (k + 0)))%nat with (2 * S k)%nat by abstract lia; apply mlarge_omega. - intro k; path_decompose (2 * (S k))%nat. + instantiate (1:= T1omega * S i). * specialize (IHi (2 * S k)%nat); rewrite iterate_rw; auto. + apply path_to_omega_mult. + clear IHi; induction i. * cbn; abstract lia. * eapply Nat.le_trans. -- eapply IHi. -- apply Nat.pred_le_mono; apply iterate_le_n_Sn; abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)