proposition: Lemma maxn_minl : left_distributive maxn minn.
proof: Proof. move=> m1 m2 n; wlog le_m21: m1 m2 / m2 <= m1. move=> IH; case/orP: (leq_total m2 m1) => /IH //. by rewrite minnC [in R in _ = R]minnC. rewrite (minn_idPr le_m21); apply/esym/minn_idPr. by rewrite geq_max leq_maxr leq_max le_m21. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring