proposition: Lemma ltn_psubCl m n p : 0 < p -> 0 < n -> (m - n < p) = (m - p < n).
proof: Proof. by move=> p_gt0 n_gt0; rewrite !ltn_psubLR // addnC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring