proposition: Lemma foo_eq n : foo n = if n < 4 then n else \max_(m <- split n) foo m.
proof: Proof. apply: (Fix_eq xpredT) => // {n} g f n _ H. rewrite /foo_rec. case: ifP => // _. apply: eq_big_seq => m /split_lt. exact: H. Qed.
imports: mathcomp(all_ssreflect)