proposition: Lemma ltZ_subRL m n p : (n < p - m) <-> (m + n < p).
proof: Proof. split => [/(@ltZ_add2l m)|H]; first by rewrite subZKC. by apply (@ltZ_add2l m); rewrite subZKC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia