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