proposition: Remark RAlim : strict_mono (H'_ alpha).
proof: Proof. intros m n H; rewrite (H'_eq3); auto. - rewrite (H'_eq3 alpha); auto. + destruct (Halpha (Canon alpha (S n))). * apply CanonS_lt; now apply Limit_not_Zero. * apply Nat.lt_le_trans with (H'_ (Canon alpha (S m)) (S m)). -- destruct (Halpha (Canon alpha (S m)) ). ++ apply CanonS_lt; now apply Limit_not_Zero. ++ apply PA1; abstract lia. -- apply Nat.le_trans with (H'_ (Canon alpha (S m)) n). destruct (Compat815.le_lt_or_eq _ _ H). ++ destruct (Halpha (Canon alpha (S m))). apply CanonS_lt; now apply Limit_not_Zero. specialize (PA1 (S m) n H0); abstract lia. ++ subst n; reflexivity. ++ apply PE0; specialize (KS_thm_2_4_E0 alpha Hlim H); intro H0; destruct n. inversion H. apply Cor12_E0 with 0. apply Canon_mono1; auto. abstract lia. abstract lia. apply KS_thm_2_4_E0; auto. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)