proposition: Remark RElim : forall beta n, Canon_plus n alpha beta -> (H'_ beta n <= H'_ alpha n)%nat.
proof: Proof. intros beta n H; destruct n. rewrite (H'_eq3 alpha); auto. - destruct H. - destruct (Canon_plus_inv H). + subst; rewrite (H'_eq3 alpha); auto. specialize (Halpha (Canon alpha (S (S n)))). destruct Halpha. * apply Canon_lt, Limit_not_Zero; auto. * apply PE0; apply Cor12_E0 with 0. -- apply Canon_mono1; auto. -- abstract lia. -- apply KS_thm_2_4_E0; auto. + destruct (Halpha (Canon alpha (S n))). apply Canon_lt, Limit_not_Zero; auto. rewrite (H'_eq3 alpha); auto. specialize (PE0 _ _ H0); auto. transitivity (H'_ (Canon alpha (S n)) (S n)); auto. destruct (Halpha (Canon alpha (S (S n)))). * apply Canon_lt, Limit_not_Zero; auto. * apply (PE1 (Canon alpha (S n))); auto with arith. apply Cor12_E0 with 0; auto with arith E0. apply Canon_mono1; auto. 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)