proposition: Remark RE : forall beta n, Canon_plus n alpha beta -> F_ beta n <= F_ alpha n.
proof: Proof. destruct n. repeat rewrite F_alpha_0_eq. reflexivity. intros. transitivity (F_ beta (S n)). rewrite alpha_def in H. - destruct (Canon_plus_first_step H). subst beta0; reflexivity. destruct (Halpha beta). rewrite alpha_def. apply Lt_Succ. apply PE0. auto. - destruct (Halpha beta). rewrite alpha_def. apply Lt_Succ. rewrite alpha_def. apply Nat.lt_le_incl. apply PD0. auto with arith. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)