proposition: Lemma replace_exponential (n : nat) : 1 + n <= 3 ^ n.
proof: Proof. elim: n => [|n HIn] // . apply: (@leq_trans (1 + 3 ^ n)); first by rewrite leq_add2l. by rewrite addnC expnS mulSn leq_add2l muln_gt0 expn_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial