proposition: Lemma pyramid_length n : n + length (pyramid n) <= 4 ^ n.
proof: Proof. elim: n; first by (move=> /=; lia). move=> n IH. rewrite /pyramid seq_last /plus -/plus flat_map_concat_map map_app concat_app app_length. rewrite -flat_map_concat_map -/(pyramid _). rewrite /map /concat app_length seq_length /=. have := Nat.pow_gt_lin_r 4 n. by lia. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun