proposition: Lemma minn_idPl {m n} : reflect (minn m n = m) (m <= n).
proof: Proof. rewrite (sameP maxn_idPr eqP) -(eqn_add2l m) eq_sym -addn_min_max eqn_add2r. exact: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring