proposition: Lemma L_omega_square_Sle : S <<= L_omega_square.
proof: Proof. intro k; destruct k. - cbn. auto with arith. - unfold L_omega_square. generalize (iterate_Sge (fun z => S (2 * z)%nat)); intro H. specialize (H k). transitivity (S (S (S k))); auto with arith. apply H. apply L_omega_Sle. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)