proposition: Lemma L_omega_square_ok: L_spec (T1omega * T1omega) L_omega_square.
proof: Proof. right; [cbn; discriminate | ]. intro k; rewrite L_omega_square_eqn1. red; path_decompose (S k). - instantiate (1 := T1omega * S k). specialize (L_omega_mult_ok (S k)). inversion 1. apply (H1 (S k)). - rewrite interval_singleton; left. + discriminate. + split. * discriminate. * simpl; f_equal; try abstract lia. - generalize (L_omega_mult_Sle k (S (S k))); abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)