proposition: Fact f1293E : f 1293 = 2022.
proof: Proof. destruct (f3nE 6) as [H1 H2]. rewrite -[2022]/(2 * 3 ^ 6 + (2022 - 2 * (3 ^ 6))). rewrite -{1}[1293]/(3 ^ 6 + (2022 - 2 * (3 ^ 6))). rewrite -[X in _ = X + _]H1. apply: eqf2D (_ : _ = _ + 3 ^ 6) _ => //. by rewrite -[3 ^ 6 + 3 ^ 6]/(2 * 3 ^ 6) H2 H1. Qed.
imports: mathcomp(all_ssreflect)