proposition: Lemma ltnfn n : 0 < n -> n < f n.
proof: Proof. move=> n_gt0. have := leqnfn n; rewrite leq_eqVlt; case: eqP => // nE _. have : f n = 3 * n by rewrite [in LHS]nE ffE. move=> /eqP; rewrite -nE -{1}(mul1n n) eqn_mul2r. by case: (n) n_gt0. Qed.
imports: mathcomp(all_ssreflect)