proposition: Lemma leq_subnK: forall m n : nat, n <= (n - m) + m.
proof: Proof. elim=> [|n IHn] m; first by rewrite addn0 subn0. rewrite subnS -addSnnS. move/(_ m) in IHn. have H := leqSpred (m - n). apply: leq_trans IHn _. exact: leq_add H _. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2