proposition: Theorem t3 : exists (K : nat), (0 < K)%N /\ forall n, (iter_lcmn n)%:Q <= (K * expn 3 n)%N%:Q.
proof: Proof. have [K [Kpos Kmaj]] := t3_nat. by exists K; split => // n; rewrite ler_nat. Qed.
imports: ZArith mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp tactics binomialz floor arithmetics posnum rat_of_Z hanson_elem_arith hanson_elem_analysis