proposition: Lemma foo_f_int (f : int -> int) (x : int) : f (1 + x) = f (x + 1).
proof: Proof. smt. Qed.
imports: Coq(ZArith Zify ZifyClasses ZifyBool ZifyInst Lia) mathcomp(all_ssreflect all_algebra) mathcomp.zify(zify) Cdcl.NOlia