proposition: Lemma dom_dom: F_ (S i) >>s F_ i.
proof: Proof. exists (S n). intros p Hp. rewrite F_S_rw. pattern p at 2; generalize Hp; induction 1. rewrite iterate_S_eqn. cbn. apply Hi'. apply Nat.lt_le_trans with (F_ i (S n)). apply R. auto with arith. apply mono_weak;auto. assert (f_gt (F_ i)). exists n. red. apply R. apply iterate_ge with n. pattern n; apply proj2_sig. auto with arith. rewrite (iterate_S_eqn). apply Hi'. rewrite (iterate_S_eqn). apply Nat.le_lt_trans with (iterate (F_ i) m (S m)). apply iterate_ge with n. pattern n; apply proj2_sig. auto with arith. assert (forall l, n <= l -> l < F_ i l). pattern n; apply proj2_sig. apply H. apply Nat.le_trans with (S m). auto with arith. apply iterate_ge with n. pattern n; apply proj2_sig. auto with arith. Qed.
imports: Coq(ArithRing Lia Arith)