proposition: Remark RAlim : strict_mono (F_ alpha).
proof: Proof. red;intros m n H; destruct m. - rewrite (F_lim_eqn alpha n);auto. rewrite F_alpha_0_eq. destruct n. inversion H. unfold Canon. apply Nat.le_lt_trans with (S n). auto with arith. destruct (Halpha (Canon alpha (S n))). apply CanonS_lt. now apply Limit_not_Zero. now apply PB0. - destruct n. inversion H. rewrite (F_lim_eqn alpha (S n));auto. rewrite (F_lim_eqn alpha (S m));auto. assert (Canon_plus 1 (Canon alpha (S n)) (Canon alpha (S m))). apply KS_thm_2_4_E0; auto. auto with arith. assert (Canon_plus (S n) (Canon alpha (S n)) (Canon alpha (S m))). eapply Cor12_E0 with 0; auto with arith. apply canonS_limit_mono; auto with T1. auto with arith. auto with E0. auto with arith. apply Nat.le_lt_trans with (F_ (Canon alpha (S n)) (S m) ). destruct (Halpha (Canon alpha (S n))). apply Canon_lt. now apply Limit_not_Zero. apply PE0. auto. auto. eapply Cor12_E0 with 0; auto with arith. apply canonS_limit_mono; auto with T1. auto with arith. destruct (Halpha (Canon alpha (S n))). apply Canon_lt. now apply Limit_not_Zero. auto with E0. auto with arith. apply PA. apply Halpha. apply CanonS_lt. auto with E0. auto with arith. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)