proposition: Lemma f3nE n : f (3 ^ n) = 2 * 3 ^ n /\ f (2 * 3 ^ n) = 3 ^ (S n).
proof: Proof. elim: n => [|n [IH1 IH2]]; first by rewrite f1E f2E. have f3SnE : f (3 ^ n.+1) = 2 * 3 ^ n.+1 . by rewrite -[in LHS]IH2 ffE mulnC -mulnA expnS [3 * _]mulnC. by split => //; rewrite -f3SnE ffE !expnS. Qed.
imports: mathcomp(all_ssreflect)