proposition: Lemma leq_min m n1 n2 : (m <= minn n1 n2) = (m <= n1) && (m <= n2).
proof: Proof. wlog le_n21: n1 n2 / n2 <= n1. by case/orP: (leq_total n2 n1) => ?; last rewrite minnC andbC; apply. rewrite /minn ltnNge le_n21 /=; case le_m_n1: (m <= n1) => //=. apply/contraFF: le_m_n1 => /leq_trans; exact. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring