proposition: Lemma lenP: forall n m, reflect (exists k, k + n = m) (len n m).
proof: Proof. move=> n; elim: n. move=> m. apply: (iffP idP). move=> _. by exists m; apply: addn0. by []. move=> n IH m. apply: (iffP idP). case: m. by []. move=> m /= le_nm. move/IH: le_nm=> le_nm. case: le_nm. move=> k eq_xk_m. exists k. by rewrite -eq_xk_m addnS. case: m. case. move=>k. by rewrite addnS. move=> m h. case: h => k. rewrite addnS. move=> eq_kSn_k. case: eq_kSn_k. move=> eq_kn_m. apply/IH. by exists k. Qed.
imports: mathcomp(all_ssreflect)