proposition: Lemma addn_pred_leqI a b k i : (a + b).-1 <= k -> i <= k -> a <= i \/ b <= k - i.
proof: Proof. move=> Hk Hi; case: (leqP a i) => Ha; [by left|right]. apply: leq_addLRI. apply: leq_trans _ Hk. apply: ltn_leq_pred. by rewrite addnC ltn_add2r. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2