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