proposition: Lemma seq_sat1 {n} : (seq 0 n) ++ [n] ~p [0] ++ (map S (seq 0 n)).
proof: Proof. have -> : S = (fun i => (S 0) + i) by done. have -> : seq 0 n = map (fun i => (S 0) * i) (seq 0 n). { elim: (seq 0 n); first done. move=> ??? /=. rewrite Nat.add_0_r. by congr cons. } have -> : [n] = [1*n] by (congr cons; lia). by apply: seq_sat2. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun