proposition: Lemma L_omega_square_smono : strict_mono L_omega_square.
proof: Proof. unfold L_omega_square. generalize (iterate_mono (fun z : nat => S (2 * z)) L_omega_smono L_omega_Sle). intros H x y Hxy. apply Nat.lt_le_trans with (iterate (fun z : nat => S (2 * z)) x (S y)). - apply iterate_mono. + apply L_omega_smono. + apply L_omega_Sle. + auto with arith. - apply Nat.lt_le_incl; apply iterate_lt; auto. * apply L_omega_smono. * apply L_omega_Sle. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)