proposition: Remark RE : forall beta n, Canon_plus n alpha beta -> (H'_ beta n <= H'_ alpha n)%nat.
proof: Proof. subst alpha; destruct n. - simpl Canon_plus; tauto. - intro H; destruct (Canon_plus_inv H). + subst beta0; destruct (Halpha beta). * apply Lt_Succ. * rewrite Canon_Succ; apply PC0. + replace (Canon (E0_succ beta) (S n)) with beta in H0. * transitivity (H'_ beta (S n)). -- destruct (Halpha beta). ++ apply Lt_Succ. ++ apply PE0; auto. -- destruct (Halpha beta). ++ apply Lt_Succ. ++ apply PC0. * now rewrite Canon_Succ. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)