proposition: Theorem contender_3_lt_contender_4 : contender_3 < contender_4.
proof: Proof. unfold contender_3, contender_4, "<". rewrite unfold_ack; [|lia]. replace (10002) with (S (S (10000))) by reflexivity. rewrite unfold_iter. transitivity (S (iter (ack 4 42) (S (Init.Nat.of_uint (Decimal.D1 (Decimal.D0 (Decimal.D0 (Decimal.D0 (Decimal.D0 Decimal.Nil))))))))). - apply le_n_S. rewrite unfold_iter. transitivity (ack 4 42 (S ((Init.Nat.of_uint (Decimal.D1 (Decimal.D0 (Decimal.D0 (Decimal.D0 (Decimal.D0 Decimal.Nil))))))))). + exact (ack_4 10000). + apply mon_ack_in_b; [lia|]. assert (geS (iter (ack 4 42))). -- apply (geS_ack 5 42); lia. -- apply H. - apply (geS_ack 4 42); lia. Qed.
imports: Arith Lia