proposition: Lemma subn_minl : left_distributive subn minn.
proof: Proof. move=> m n p; apply/eqP. rewrite eqn_leq !leq_min !leq_sub2r geq_min ?leqnn ?orbT //= /minn. by case: (_ < _); rewrite leqnn // orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring