proposition: Lemma eqn_sub2lE m n p : p <= m -> n <= m -> (m - p == m - n) = (p == n).
proof: Proof. by move=> pm nm; rewrite !eqn_leq !leq_sub2lE // -!eqn_leq eq_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring