proposition: Lemma path_to_omega_mult (i k:nat) : path_to (T1omega * i) (interval (S k) (2 * (S k))%nat) (T1omega * (S i)).
proof: Proof. destruct i. - simpl; apply mlarge_omega. - path_decompose (S k). instantiate (1:=T1.cons one i (S k)). + simpl (T1omega * S i). replace (i + 0)%nat with i. apply path_to_tail; auto with T1. * assert (H := mlarge_FS k (S k)). replace (2 * S k)%nat with (S (k + S k))%nat by lia; auto. * abstract lia. + rewrite interval_singleton; left; [discriminate | ]. simpl; replace (i + 0)%nat with i. split; [ discriminate | reflexivity]. abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)