proposition: Theorem contender_1_lt_contender_2 : contender_1 < contender_2.
proof: Proof. Time cbv delta [contender_1 contender_2]; repeat match goal with | _ => progress eapply Nat.pow_lt_mono_r; [solve [lia]|] | |- ?x < ?y => match y with | context[x ^ x] => progress erewrite <-Nat.pow_1_r at 1 end | _ => progress eapply Nat.pow_gt_1; [solve [lia]|] | _ => progress eapply Nat.pow_nonzero; solve [lia] end. Time Qed. Opaque Nat.pow. Definition tower_of_power (n : nat) : nat := Nat.recursion 42 (fun _ k => 42 ^ k) n. Ltac depth t := match constr:(t) with | 42 => constr:(0) | ?x ^ ?y => let d := depth y in constr:(S d) | _ => fail end. Ltac reify_tower t := match constr:(t) with | _ ^ _ => let d := depth t in constr:(tower_of_power d) | _ => fail end. Ltac reify_goal := match goal with | [ |- ?x < ?y ] => let t := (reify_tower x) in replace x with t by reflexivity end. Definition contender_3 := tower_of_power 10000. Lemma fund_lemma : forall n m, n < m -> tower_of_power n < tower_of_power m. Proof. intros. induction H. - simpl. apply Nat.pow_gt_lin_r; lia. - simpl. assert (42 ^ tower_of_power n < 42 ^ tower_of_power m) by (apply Nat.pow_lt_mono_r; lia). eapply Nat.lt_trans; [exact IHle|]. apply Nat.pow_gt_lin_r; lia. Qed.
imports: Arith Lia