proposition: Lemma F_rec_narrow m n x : P x -> measure x < n -> n <= m -> F_rec m x = F_rec n x.
proof: Proof. elim: n m x => // => n IHn [//|m] x Px A B /=. apply: F_wf => // y Py Hy. apply: IHn => //. exact: leq_trans Hy _. Qed.
imports: mathcomp(all_ssreflect)