proposition: Remark Rem3 : forall n, Ack m.+1 n <= Ack m.+2 n.
proof: Proof. destruct Hm as [H1 [H2 H3]]. intro n; simpl (Ack m.+2 n); simpl (Ack m.+1 n). apply Ack_m_mono_weak. apply iterate_le_np_le. - intro p; transitivity p.+1; auto. - transitivity n.+1; auto. replace n.+1 with (iterate S n 1). + apply iterate_mono_1 with 0; auto. * intros x y H; auto with arith. * intro x; auto. * intros; generalize (Rem2 n0); auto. + induction n; cbn; auto. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)