proposition: Remark R1 : strict_mono (F_ alpha).
proof: Proof. destruct (Halpha beta). subst alpha; apply Lt_Succ. red; intros. subst alpha. repeat rewrite F_succ_eqn. induction H. rewrite (iterate_S_eqn (F_ beta) (S n)). apply Nat.lt_le_trans with (F_ beta (iterate (F_ beta) (S n) n)). auto. apply mono_weak; auto. apply Nat.lt_le_incl. apply iterate_mono;auto. destruct (Halpha beta). apply Lt_Succ. transitivity (iterate (F_ beta) (S m) m);auto. rewrite (iterate_S_eqn (F_ beta) (S m)). apply Nat.lt_le_trans with (F_ beta (iterate (F_ beta) (S m) m)). auto. apply mono_weak; auto. apply Nat.lt_le_incl. apply iterate_mono;auto. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)